ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Automatic verification of finite-state concurrent systems using temporal logic specifications
Full text PdfPdf (1.40 MB)
Source ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 8 ,  Issue 2  (April 1986) table of contents
Pages: 244 - 263  
Year of Publication: 1986
ISSN:0164-0925
Authors
E. M. Clarke  Carnegie Mellon Univ.
E. A. Emerson  Univ. of Texas, Austin
A. P. Sistla  GTE Laboratories, Inc.
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 44,   Downloads (12 Months): 493,   Citation Count: 391
Additional Information:

abstract   references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/5397.5399
What is a DOI?

ABSTRACT

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.


REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
BEN-ARI, M., PNUELI, A., AND MANNA, Z. The temporal logic of branching time. Acta In{. 20 (1983), 207-226.
2
K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969  [doi>10.1145/362946.362970]
 
3
Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
 
4
E. Allen Emerson , Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.169-181, July 14-18, 1980
5
E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986  [doi>10.1145/4904.4999]
 
6
EMERSON, E. A., AND CLARKE, E. M. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2 (1982), 241-266.
7
E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States  [doi>10.1145/318593.318620]
8
Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada  [doi>10.1145/567446.567462]
 
9
R. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
10
C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978  [doi>10.1145/359576.359585]
11
Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada  [doi>10.1145/567446.567463]
 
12
Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
 
13
MANNA, Z., AND PNUELI, A. Verification of concurrent programs: The temporal framework. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds., Academic Press, London, 1981, 215-273.
14
Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984  [doi>10.1145/357233.357237]
15
Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982  [doi>10.1145/357172.357178]
 
16
Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
 
17
QUIELLE, J. P., AND SIFAK1S, J. Fairness and related properties in transition systems. 292, IMAG, Univ. of Grenoble, Mar. 1982.
18
A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985  [doi>10.1145/3828.3837]
 
19
ZAFIROPULO, P., WEST, C., RUDIN, H., COWAN, D., AND BRAND, D. Towards analyzing and synthesizing protocols. IEEE Trans. Commun. COM-28, 4 (Apr. 1980), 651-671.

CITED BY  391
Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999
Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992
Jeannette M. Wing , Chun Gong, Experience with the Larch Prover, ACM SIGSOFT Software Engineering Notes, v.15 n.4, p.140-143, Sep. 1990
Michal Young , Richard N. Taylor , David L. Levine , Kari A. Nies , Debra Brodbeck, A concurrency analysis tool suite for Ada programs: rationale, design, and preliminary experience, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.1, p.65-106, Jan. 1995
Daniel Jackson , Craig A. Damon, Elements of style: analyzing a software design feature with a counterexample detector, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.239-249, May 1996
Zhiming Liu , Mathai Joseph, Specification and verification of fault-tolerance, timing, and scheduling, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.46-89, Jan. 1999
S. Campos , E. Clarke , W. Marrero , M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems, ACM SIGPLAN Notices, v.30 n.11, p.70-78, Nov. 1995
Rance Cleaveland , Scott A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys (CSUR), v.28 n.4, p.607-625, Dec. 1996
Xudong He , Junhua Ding , Yi Deng, Model checking software architecture specifications in SAM, Proceedings of the 14th international conference on Software engineering and knowledge engineering, July 15-19, 2002, Ischia, Italy
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States
Paul F. Syverson, Adding time to a logic of authentication, Proceedings of the 1st ACM conference on Computer and communications security, p.97-101, November 03-05, 1993, Fairfax, Virginia, United States
Massimiliano Chiodo , Thomas R. Shiple , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic compositional minimization in CTL model checking, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.172-178, November 1992, Santa Clara, California, United States
Olaf Burkart , Bernhard Steffen, Composition, decomposition and model checking of pushdown processes, Nordic Journal of Computing, v.2 n.2, p.89-125, Summer 1995
Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, Proceedings of the 14th international conference on Software engineering, p.199-211, May 11-15, 1992, Melbourne, Australia
Tevfik Bultan , Jeffrey Fischer , Richard Gerber, Compositional verification by model checking for counter-examples, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.224-238, May 1996
Tevfik Bultan, Action Language: a specification language for model checking reactive systems, Proceedings of the 22nd international conference on Software engineering, p.335-344, June 04-11, 2000, Limerick, Ireland
Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996
Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995
P. -Y. Schobbens , J. -F. Raskin , T. A. Henzinger, Axioms for real-time logics, Theoretical Computer Science, v.274 n.1-2, p.151-182, March 6, 2002
Tod Amon , Gaetano Borriello, OEsim: a simulator for timing behavior, Proceedings of the 28th conference on ACM/IEEE design automation, p.656-661, June 17-22, 1991, San Francisco, California, United States
Daniel Kroening , Wolfgang J. Paul, Automated pipeline design, Proceedings of the 38th conference on Design automation, p.810-815, June 2001, Las Vegas, Nevada, United States
Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000
William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States
R. Sekar , C. R. Ramakrishnan , I. V. Ramakrishnan , S. A. Smolka, Model-Carrying Code (MCC): a new paradigm for mobile-code security, Proceedings of the 2001 workshop on New security paradigms, September 10-13, 2001, Cloudcroft, New Mexico
Ramin Hojati , Thomas R. Shiple , Robert K. Brayton , Robert P. Kurshan, A unified approach to language containment and fair CTL model checking, Proceedings of the 30th international conference on Design automation, p.475-481, June 14-18, 1993, Dallas, Texas, United States
S. Aggarwal , C. Courcoubetis , P. Wolper, Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.303-339, April 1990
K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States
Amit Goel , William R. Lee, Formal verification of an IBM CoreConnect processor local bus arbiter core, Proceedings of the 37th conference on Design automation, p.196-200, June 05-09, 2000, Los Angeles, California, United States
James R. Larus, Whole program paths, ACM SIGPLAN Notices, v.34 n.5, p.259-269, May 1999
Arie Gurfinkel , Benet Devereux , Marsha Chechik, Model exploration with temporal logic query checking, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
Linda Ness, L.0: a parallel executable temporal logic language, ACM SIGSOFT Software Engineering Notes, v.15 n.4, p.80-89, Sep. 1990
Peter Buchholz , Peter Kemper, Hierarchical Reachability Graph Generation for Petri Nets, Formal Methods in System Design, v.21 n.3, p.281-315, November 2002
Allen Emerson , Jai Srinivasan, A decidable temporal logic to reason about many processes, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.233-246, August 22-24, 1990, Quebec City, Quebec, Canada
Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
Rajnish Ghughal , Abdel Mokkedem , Ratan Nalumasu , Ganesh Gopalakrishnan, Using “test model-checking” to verify the Runway-PA8000 memory model, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.231-239, June 28-July 02, 1998, Puerto Vallarta, Mexico
Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996
David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Proving correctness of compiler optimizations by temporal logic, ACM SIGPLAN Notices, v.37 n.1, p.283-294, Jan. 2002
Enrico Vicario, Static Analysis and Dynamic Steering of Time-Dependent Systems, IEEE Transactions on Software Engineering, v.27 n.8, p.728-748, August 2001
R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States
Thomas A. Henzinger , Orna Kupferman , Sriram K. Rajamani, Fair simulation, Information and Computation, v.173 n.1, p.64-81, February 25, 2002
Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States
Gregory D. Abowd , Hung-Ming Wang , Andrew F. Monk, A formal technique for automated dialogue development, Proceedings of the conference on Designing interactive systems: processes, practices, methods, & techniques, p.219-226, August 23-25, 1995, Ann Arbor, Michigan, United States
Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States
Steven M. Burns , Henrik Hulgaard , Tod Amon , Gaetano Borriello, An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems, IEEE Transactions on Computers, v.44 n.11, p.1306-1317, November 1995
P. David Stotts , Richard Furuta , J. Cyrano Ruiz, Hyperdocuments as automata: trace-based browsing property verification, Proceedings of the ACM conference on Hypertext, p.272-281, November 30-December 04, 1992, Milan, Italy
K. Olender , L. Osterweil, Cesar: a static sequencing constraint analyzer, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.66-74, Dec. 1989
J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States
Mats P. E. Heimdahl , Nancy G. Leveson, Completeness and consistency analysis of state-based requirements, Proceedings of the 17th international conference on Software engineering, p.3-14, April 24-28, 1995, Seattle, Washington, United States
W. Howden, Validating programs without specifications, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.2-9, Dec. 1989
Duncan Clarke , Insup Lee, Testing real-time constraints in a process algebraic setting, Proceedings of the 17th international conference on Software engineering, p.51-60, April 24-28, 1995, Seattle, Washington, United States
William Chan , Richard J. Anderson , Paul Beame , David Notkin, Improving efficiency of symbolic model checking for state-based system requirements, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.102-112, March 1998
David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States
Shing Chi Cheung , Jeff Kramer, Context constraints for compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.334-377, Oct. 1996
P. Ladkin, Specification of time dependencies and synthesis of concurrent processes, Proceedings of the 9th international conference on Software Engineering, p.106-115, March 1987, Monterey, California, United States
Joseph Y. Halpern , Lenore D. Zuck, A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols, Journal of the ACM (JACM), v.39 n.3, p.449-478, July 1992
Jean Berstel , Stefano Crespi Reghizzi , Gilles Roussel , Pierluigi San Pietro, A scalable formal method for design and automatic checking of user interfaces, Proceedings of the 23rd International Conference on Software Engineering, p.453-462, May 12-19, 2001, Toronto, Ontario, Canada
Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992
Robert J. Allen , David Garlan , James Ivers, Formal modeling and analysis of the HLA component integration standard, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.70-79, Nov. 1998
Jeremy Levitt , Kunle Olukotun, A scalable formal verification methodology for pipelined microprocessors, Proceedings of the 33rd annual conference on Design automation, p.558-563, June 03-07, 1996, Las Vegas, Nevada, United States
Joanne M. Atlee , John Gannon, Analyzing timing requirements, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.117-127, July 1993
L. K. Dillon , Y. S. Ramakrishna, Generating oracles from your favorite temporal logic specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.106-117, Nov. 1996
Moshe Y. Vardi, On the complexity of bounded-variable queries (extended abstract), Proceedings of the fourteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.266-276, May 22-25, 1995, San Jose, California, United States
P. David Stotts , Richard Furuta , Cyrano Ruiz Cabarrus, Hyperdocuments as automata: verification of trace-based browsing properties by model checking, ACM Transactions on Information Systems (TOIS), v.16 n.1, p.1-30, Jan. 1998
Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada
Hiroaki Iwashita , Tsuneo Nakata, Forward model checking techniques oriented to buggy designs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.400-404, November 09-13, 1997, San Jose, California, United States
Robyn R. Lutz , Johnny S. K. Wong, Detecting Unsafe Error Recovery Schedules, IEEE Transactions on Software Engineering, v.18 n.8, p.749-760, August 1992
Kathi Fisler , Shriram Krishnamurthi, Modular verification of collaboration-based software designs, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993
Fuyau Lin, A formalism for specifying communicating processes, Proceedings of the 1993 ACM conference on Computer science, p.123-130, February 16-18, 1993, Indianapolis, Indiana, United States
M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.200-209, Dec. 1989
C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States
R. E. Kurt Stirewalt , Laura K. Dillon, A component-based approach to building formal analysis tools, Proceedings of the 23rd International Conference on Software Engineering, p.167-176, May 12-19, 2001, Toronto, Ontario, Canada
Joanne Atlee , John Gannon, State-based model checking of event-driven system requirements, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.16-28, Dec. 1991
Dynamic documents over the Web, Advances in software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
Steve Easterbrook , Marsha Chechik, A framework for multi-valued reasoning over inconsistent viewpoints, Proceedings of the 23rd International Conference on Software Engineering, p.411-420, May 12-19, 2001, Toronto, Ontario, Canada
Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
M. Felder , D. Mandrioli , A. Morzenti, Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models, IEEE Transactions on Software Engineering, v.20 n.2, p.127-141, February 1994
Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland
W. E. Howden , G. M. Shi, Linear and structural event sequence analysis, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.98-106, May 1996
L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997
P. Breuer , C. Delgado Kloos , N. Martínez Madrid , L. Sánchez , A. Marín, A refinement calculus for VHDL, Proceedings of the conference on European design automation, p.482-487, September 1996, Geneva, Switzerland
Kurt M. Olender , Leon J. Osterweil, Interprocedural static analysis of sequencing constraints, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.1, p.21-52, Jan. 1992
P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000
Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.156-166, Nov. 1996
Fong Pong , Michel Dubois, The verification of cache coherence protocols, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.11-20, June 30-July 02, 1993, Velen, Germany
Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994
Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
Gleb Naumovich , Lori A. Clarke, Classifying properties: an alternative to the safety-liveness classification, ACM SIGSOFT Software Engineering Notes, v.25 n.6, p.159-168, Nov. 2000
Dimitra Giannakopoulou , Jeff Magee , Jeff Kramer, Checking progress with action priority: is it fair?, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.511-527, Nov. 1999
Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
P. Ciancarini , F. Franzé , C. Mascolo, Using a coordination language to specify and analyze systems containing mobile components, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.2, p.167-198, April 2000
E. M. Clarke , O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.294-303, August 10-12, 1987, Vancouver, British Columbia, Canada
Joanne M. Atlee , Michael A. Buckley, A logic-model semantics for SCR software requirements, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.280-292, May 1996
Michael Young , Richard N. Taylor, Rethinking the taxonomy of fault detection techniques, Proceedings of the 11th international conference on Software engineering, p.53-62, May 1989, Pittsburgh, Pennsylvania, United States
Manish Pandey , Richard Raimi , Derek L. Beatty , Randal E. Bryant, Formal verification of PowerPC arrays using symbolic trajectory evaluation, Proceedings of the 33rd annual conference on Design automation, p.649-654, June 03-07, 1996, Las Vegas, Nevada, United States
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
Narayanan Krishnamurthy , Magdy S. Abadir , Andrew K. Martin , Jacob A. Abraham, Design and Development Paradigm for Industrial Formal Verification CAD Tools, IEEE Design & Test, v.18 n.4, p.26-35, July 2001
Harry Li , Shriram Krishnamurthi , Kathi Fisler, Verifying cross-cutting features as open systems, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July 2003
Narayanan Krishnamurthy , Andrew K. Martin , Magdy S. Abadir , Jacob A. Abraham, Validating PowerPC Microprocessor Custom Memories, IEEE Design & Test, v.17 n.4, p.61-76, October 2000
Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.308-339, Oct. 1994
Chuchang Liu , Mehmet A. Orgun, Executing specifications of distributed computations with Chronolog(MC), Proceedings of the 1996 ACM symposium on Applied Computing, p.393-400, February 17-19, 1996, Philadelphia, Pennsylvania, United States
Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
Marsha Chechik, SC(R)3: towards usability of formal methods, Proceedings of the 1998 conference of the Centre for Advanced Studies on Collaborative research, p.8, November 30-December 03, 1998, Toronto, Ontario, Canada
Marie-Claude Gaudel, Formal specification techniques (extended abstract), Proceedings of the 16th international conference on Software engineering, p.223-227, May 16-21, 1994, Sorrento, Italy
Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
Mauro Pezzè , Richard N. Taylor , Michal Young, Graph models for reachability analysis of concurrent programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.171-213, April 1995
Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.62-75, Dec. 1994
Ahmed Bouajjani , Rachid Echahed , Peter Habermehl, Verifying infinite state processes with sequential and parallel composition, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-106, January 23-25, 1995, San Francisco, California, United States
Françoise Casaubieilh , Anthony McIsaac , Mike Benjamin , Mike Bartley , François Pogodalla , Frédéric Rocheteau , Mohamed Belhadj , Jeremy Eggleton , Gérard Mas , Geoff Barrett , Christian Berthet, Functional verification methodology of Chameleon processor, Proceedings of the 33rd annual conference on Design automation, p.421-426, June 03-07, 1996, Las Vegas, Nevada, United States
Hasan Davulcu , Michael Kifer , C. R. Ramakrishnan , I. V. Ramakrishnan, Logic based modeling and analysis of workflows, Proceedings of the seventeenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.25-33, June 01-04, 1998, Seattle, Washington, United States
Pierre Wolper, Constructing automata from temporal logic formulas: a tutorial, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
Laura K. Dillon , Qing Yu, Oracles for checking temporal properties of concurrent systems, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.140-153, Dec. 1994
Alessandro Aldini , Marco Bernardo , Roberto Gorrieri , Marco Roccetti, Comparing the QoS of Internet audio mechanisms via formal methods, ACM Transactions on Modeling and Computer Simulation (TOMACS), v.11 n.1, p.1-42, Jan. 2001
F. Kabanza , J.-M. Stevenne , P. Wolper, Handling infinite temporal data, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.392-403, April 02-04, 1990, Nashville, Tennessee, United States
E. M. Clarke , M. Khaira , X. Zhao, Word level model checking—avoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States
Luis Alejandro Cortés , Petru Eles , Zebo Peng, Verification of embedded systems using a petri net based representation, Proceedings of the 13th international symposium on System synthesis, September 20-22, 2000, Madrid, Spain
Robert Allen , David Garlan, Formalizing architectural connection, Proceedings of the 16th international conference on Software engineering, p.71-80, May 16-21, 1994, Sorrento, Italy
E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States
David Lesens , Nicolas Halbwachs , Pascal Raymond, Automatic verification of parameterized linear networks of processes, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-357, January 15-17, 1997, Paris, France
Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997
J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993
Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994
Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997
Christophe Ratel , Nicolas Halbwachs , Pascal Raymond, Programming and verifying critical systems by means of the synchronous data-flow language LUSTRE, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.112-119, Dec. 1991
Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996
Teodor Rus , Eric Van Wyk , Tom Halverson, Generating Model Checkers from Algebraic Specifications, Formal Methods in System Design, v.20 n.3, p.249-284, May 2002
Ratan Nalumasu , Ganesh Gopalakrishnan, An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation, Formal Methods in System Design, v.20 n.3, p.231-247, May 2002
Richard Raimi , James Lear, Silicon Debug of a PowerPC™ Microprocessor Using Model Checking, Formal Methods in System Design, v.21 n.1, p.79-94, July 2002
Paulo J. F. Carreira , Miguel E. F. Costa, Automatically verifying an object-oriented specification of the steam-boiler system, Science of Computer Programming, v.46 n.3, p.197-217, March 2003
Yung-Te Lai , Massoud Pedram , Sarma B. K. Vrudhula, Formal Verification Using Edge-Valued Binary Decision Diagrams, IEEE Transactions on Computers, v.45 n.2, p.247-255, February 1996
Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
Sergey Berezin , Edmund Clarke , Armin Biere , Yunshan Zhu, Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function, Formal Methods in System Design, v.20 n.2, p.159-186, March 2002
Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
C. R. Ramakrishnan , R. Sekar, Model-based analysis of configuration vulnerabilities, Journal of Computer Security, v.10 n.1-2, p.189-209, 2002
Xudong He , Huiqun Yu , Tianjun Shi , Junhua Ding , Yi Deng, Formally analyzing software architectural specifications using SAM, Journal of Systems and Software, v.71 n.1-2, p.11-29, April 2004
A. M. K. Cheng , J. C. Browne , A. K. Mok , Rwo-Hsi Wang, Analysis of Real-Time Rule-Based Systems with Behavioral Constraint Assertions Specified in Estella, IEEE Transactions on Software Engineering, v.19 n.9, p.863-885, September 1993
Arindam Chakrabarti , Pallab Dasgupta , P. P. Chakrabarti , Ansuman Banerjee, Formal verification of module interfaces against real time specifications, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Boudewijn R. Haverkort, Markovian models for performance and dependability evaluation, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
William N. Robinson , Suzanne D. Pawlowski , Vecheslav Volkov, Requirements interaction management, ACM Computing Surveys (CSUR), v.35 n.2, p.132-190, June 2003
José Creissac Campos, A formal approach to the usability engineering, Proceedings of the Latin American conference on Human-computer interaction, August 17-20, 2003, Rio de Janeiro, Brazil
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
Alberto Del Bimbo , Enrico Vicario , Daniele Zingoni, Symbolic Description and Visual Querying of Image Sequences Using Spatio-Temporal Logic, IEEE Transactions on Knowledge and Data Engineering, v.7 n.4, p.609-622, August 1995
Marsha Chechik , Wei Ding, Lightweight reasoning about program correctness, Proceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research, p.1, November 05-07, 2001, Toronto, Ontario, Canada
Beata Konikowska , Wojciech Penczek, Model checking for multi-valued computation tree logics, Beyond two: theory and applications of multiple-valued logic, Physica-Verlag GmbH, Heidelberg, Germany, 2003
Karsten Schmidt, Distributed verification with LoLA, Fundamenta Informaticae, v.54 n.2-3, p.253-262, February 2003
Mathias Broxvall , Peter Jonsson, Point algebras for temporal reasoning: algorithms and complexity, Artificial Intelligence, v.149 n.2, p.179-220, October 2003
Alberto Del Bimbo , Enrico Vicario, Visual Programming of Virtual Worlds Animation, IEEE MultiMedia, v.3 n.1, p.40-49, January 1996
Farn Wang, Parametric Analysis of Computer Systems, Formal Methods in System Design, v.17 n.1, p.39-60, Aug. 2000
Nazanin Mansouri , Ranga Vemuri, Automated Correctness Condition Generation for Formal Verification ofSynthesized RTL Designs, Formal Methods in System Design, v.16 n.1, p.59-91, Jan 1,2000
Tatsuhiro Tsuchiya , Shin'ichi Nagano , Rohayu Bt Paidi , Tohru Kikuno, Symbolic Model Checking for Self-Stabilizing Algorithms, IEEE Transactions on Parallel and Distributed Systems, v.12 n.1, p.81-95, January 2001
Luis Alejandro Cortés , Petru Eles , Zebo Peng, Modeling and formal verification of embedded systems based on a Petri net representation, Journal of Systems Architecture: the EUROMICRO Journal, v.49 n.12-15, p.571-598, December 2003
Lars Michael Kristensen , Søren Christensen, Implementing Coloured Petri Nets Using a Functional Programming Language, Higher-Order and Symbolic Computation, v.17 n.3, p.207-243, September 2004
Mariano P. Consens , Masum Z. Hasan , Alberto O. Mendelzon, Using Hy+ for network management and distributed debugging, Proceedings of the 1993 conference of the Centre for Advanced Studies on Collaborative research: software engineering, October 24-28, 1993, Toronto, Ontario, Canada
David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Compiler Optimization Correctness by Temporal Logic, Higher-Order and Symbolic Computation, v.17 n.3, p.173-206, September 2004
Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
Richard Raimi , Ramin Hojati , Kedar S. Namjoshi, Environment modeling and language universality, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.5 n.3, p.705-725, July 2000
Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States
David Lee , Mihalis Yannakakis, Online minimization of transition systems (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, p.264-274, May 04-06, 1992, Victoria, British Columbia, Canada
Paul C. Attie , E. Allen Emerson, Synthesis of concurrent systems with many similar processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.51-115, Jan. 1998
J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States
Roberto Barbuti , Nicoletta De Francesco , Antonella Santone , Gigiola Vaglini, Logic Based Abstractions of Real-Time Systems, Formal Methods in System Design, v.17 n.3, p.201-220, Dec. 2000
Oscar Nierstrasz, Regular types for active objects, ACM SIGPLAN Notices, v.28 n.10, p.1-15, Oct. 1, 1993
A. Aziz , F. Balarin , S.-T. Cheng , R. Hojati , T. Kam , S. C. Krishnan , R. K. Ranjan , T. R. Shiple , V. Singhal , S. Tasiran , H.-Y. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, HSIS: a BDD-based environment for formal verification, Proceedings of the 31st annual conference on Design automation, p.454-459, June 06-10, 1994, San Diego, California, United States
Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.113-123, March 1998
Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000
Matthew B. Dwyer , Corina S. Pasareanu, Filter-based model checking of partial systems, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.189-202, Nov. 1998
Irène Guessarian , Eugénie Foustoucos , Theodore Andronikos , Foto Afrati, On temporal logic versus datalog, Theoretical Computer Science, v.303 n.1, p.103-133, 28 June 2003
Gleb N. Naumovich , Lori A. Clarke , Leon J. Osterweil, Verification of communication protocols using data flow analysis, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.93-105, Nov. 1996
R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
Axel van Lamsweerde , Laurent Willemet, Inferring Declarative Requirements Specifications from Operational Scenarios, IEEE Transactions on Software Engineering, v.24 n.12, p.1089-1114, December 1998
Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States
Patrick Cousot , Radhia Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-25, January 19-21, 2000, Boston, MA, USA
Jie Xing , Munindar P. Singh, Formalization of commitment-based agent interaction, Proceedings of the 2001 ACM symposium on Applied computing, p.115-120, March 2001, Las Vegas, Nevada, United States
Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.124-133, March 1998
Arie Gurfinkel , Benet Devereux , Marsha Chechik, Model exploration with temporal logic query checking, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
Abhik Roychoudhury , Tulika Mitra, Specifying multithreaded Java semantics for program verification, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
Radu Mateescu , Mihaela Sighireanu, Efficient on-the-fly model-checking for regular alternation-free mu-calculus, Science of Computer Programming, v.46 n.3, p.255-281, March 2003
Jeff Kramer, Distributed software engineering, Proceedings of the 16th international conference on Software engineering, p.253-263, May 16-21, 1994, Sorrento, Italy
R. E. Kurt Stirewalt , Laura K. Dillon, Generation of visitor components that implement program transformations, ACM SIGSOFT Software Engineering Notes, v.26 n.3, p.86-94, May 2001
Maher Mneimneh , Karem Sakallah, SAT-based sequential depth computation, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
Mats P. E. Heimdahl , Nancy G. Leveson, Completeness and Consistency in Hierarchical State-Based Requirements, IEEE Transactions on Software Engineering, v.22 n.6, p.363-377, June 1996
David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
Gerald M. Karam , Raymond J. A. Buhr, Temporal Logic-Based Deadlock Analysis for Ada, IEEE Transactions on Software Engineering, v.17 n.10, p.1109-1125, October 1991
George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991
Harry Li , Shriram Krishnamurthi , Kathi Fisler, Verifying cross-cutting features as open systems, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
Marsha Chechik , Benet Devereux , Steve Easterbrook , Arie Gurfinkel, Multi-valued symbolic model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.371-408, October 2003
Parosh Aziz Abdulla , S. Purushothaman Iyer , Aletta Nylén, SAT-Solving the Coverability Problem for Petri Nets, Formal Methods in System Design, v.24 n.1, p.25-43, January 2004
Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990
Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE, IEEE Transactions on Software Engineering, v.18 n.9, p.785-793, September 1992
Sol M. Shatz, Towards Complexity Metrics for Ada Tasking, IEEE Transactions on Software Engineering, v.14 n.8, p.1122-1127, August 1988
Jeng-Rung Chen , Albert Mo Kim Cheng, Response Time Analysis of EQL Real-Time Rule-Based Systems, IEEE Transactions on Knowledge and Data Engineering, v.7 n.1, p.26-43, February 1995
Giacomo Bucci , Enrico Vicario, Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets, IEEE Transactions on Software Engineering, v.21 n.12, p.969-992, December 1995
Parosh Aziz Abdulla , Bengt Jonsson, Model checking of systems with many identical timed processes, Theoretical Computer Science, v.290 n.1, p.241-264, 1 January 2003
A. Prasad Sistla , Patrice Godefroid, Symmetry and reduced symmetry in model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.4, p.702-734, July 2004
S. Chaki , E. Clarke , A. Groce , J. Ouaknine , O. Strichman , K. Yorav, Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design, v.25 n.2-3, p.129-166, September-November 2004
Andrzej Skowron , Piotr Synak, Reasoning in information maps, Fundamenta Informaticae, v.59 n.2-3, p.241-259, February 2004
Hasan Davulcu , Michael Kifer , I. V. Ramakrishnan, CTR-S: a logic for specifying contracts in semantic web services, Proceedings of the 13th international World Wide Web conference on Alternate track papers & posters, May 19-21, 2004, New York, NY, USA
Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
Marcelo Sihman , Shmuel Katz, A calculus of superimpositions for distributed systems, Proceedings of the 1st international conference on Aspect-oriented software development, April 22-26, 2002, Enschede, The Netherlands
Sérgio Campos , Edmund M. Clarke , Orna Grumberg, Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System, Formal Methods in System Design, v.17 n.2, p.163-192, Oct. 2000
Paul Caspi , Alain Girault , Daniel Pilaud, Automatic Distribution of Reactive Systems for Asynchronous Networks of Processors, IEEE Transactions on Software Engineering, v.25 n.3, p.416-427, May 1999
Moshe Y. Vardi, Implementing knowledge-based programs, Proceedings of the 6th conference on Theoretical aspects of rationality and knowledge, March 17-20, 1996, The Netherlands
Alexander Holt , Ewan Klein, A semantically-derived subset of English for hardware verification, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.451-456, June 20-26, 1999, College Park, Maryland
Adnan Aziz , Thomas Shiple , Vigyan Singhal , Robert Brayton , Alberto Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking, Formal Methods in System Design, v.21 n.2, p.193-224, September 2002
Nevin Heintze , J. D. Tygar, A Model for Secure Protocols and Their Compositions, IEEE Transactions on Software Engineering, v.22 n.1, p.16-30, January 1996
Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
Hardi Hungar , Bernhard Steffen, Local model checking for context-free processes, Nordic Journal of Computing, v.1 n.3, p.364-385, Fall 1994
Marsha Chechik , John Gannon, Automatic Analysis of Consistency between Requirements and Designs, IEEE Transactions on Software Engineering, v.27 n.7, p.651-672, July 2001
A. Cimatti , M. Roveri , P. Bertoli, Conformant planning via symbolic model checking and heuristic search, Artificial Intelligence, v.159 n.1-2, p.127-206, November 2004
Haiping Xu , Sol M. Shatz, A Framework for Model-Based Design of Agent-Oriented Software, IEEE Transactions on Software Engineering, v.29 n.1, p.15-30, January 2003
Jan Van Katwijk , Ruud De Rooij , Sylvia Stuurman , Hans Toetenel, Software development and verification of dynamic real-time distributed systems based on the radio broadcast paradigm, Parallel and distributed real-time systems, Nova Science Publishers, Inc., Commack, NY, 2001
Deborah Shands , Chung-Kuo Chang, Characterizing distributed systems using knowledge-based models: preliminary version, Proceedings of the 4th conference on Theoretical aspects of reasoning about knowledge, p.29-42, March 22-25, 1992, Monterey, California
D. M. Goldschlag, Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove, IEEE Transactions on Software Engineering, v.16 n.9, p.1005-1023, September 1990
Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996
M. Lusini , E. Vicario, Engineering the usability of visual formalisms: a case study in real time logics, Proceedings of the working conference on Advanced visual interfaces, May 24-27, 1998, L'Aquila, Italy
Axel van Lamsweerde , Emmanual Letier , Robert Darimont, Managing Conflicts in Goal-Driven Requirements Engineering, IEEE Transactions on Software Engineering, v.24 n.11, p.908-926, November 1998
Jan Broersen , Leender van der Torre, Review of "Agency and deontic logic by John Horty" Oxford university press 2001, Artificial Intelligence and Law, v.11 n.1, p.45-61, January 2003
Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
Teodor Rus, A unified language processing methodology, Theoretical Computer Science, v.281 n.1-2, p.499-536, June 3 2002
Ronald Fagin , Joseph Y. Halpern , Yoram Moses , Moshe Y. Vardi, Knowledge-based programs, Distributed Computing, v.10 n.4, p.199-225, July 1997
J. S. Ostroff, Deciding Properties of Timed Transition Models, IEEE Transactions on Parallel and Distributed Systems, v.1 n.2, p.170-183, April 1990
Alberto Del Bimbo , Enrico Vicario, Specification by-Example of Virtual Agents Behavior, IEEE Transactions on Visualization and Computer Graphics, v.1 n.4, p.350-360, December 1995
Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004
Stephen F. Seigel , George S. Avrunin, Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles, IEEE Transactions on Software Engineering, v.28 n.2, p.115-128, February 2002
Fong Pong , Michel Dubois, A New Approach for the Verification of Cache Coherence Protocols, IEEE Transactions on Parallel and Distributed Systems, v.6 n.8, p.773-787, August 1995
Gaoyan Xie , Cheng Li , Zhe Dang, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Theoretical Computer Science, v.328 n.1-2, p.203-219, 29 November 2004
Jia Xu, On Inspection and Verification of Software with Timing Requirements, IEEE Transactions on Software Engineering, v.29 n.8, p.705-720, August 2003
Serge Abiteboul , Zoë Abrams , Stefan Haar , Tova Milo, Diagnosis of asynchronous discrete event systems: datalog to the rescue!, Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 13-15, 2005, Baltimore, Maryland
Vincenzo Gervasi , Didar Zowghi, Reasoning about inconsistencies in natural language requirements, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.3, p.277-330, July 2005
Sascha Konrad , Betty H. C. Cheng, Real-time specification patterns, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
David Stotts , Jaime Navon, Model checking cobweb protocols for verification of HTML frames behavior, Proceedings of the 11th international conference on World Wide Web, May 07-11, 2002, Honolulu, Hawaii, USA
Jean Berstel , Stefano Crespi Reghizzi , Gilles Roussel , Pierluigi San Pietro, A scalable formal method for design and automatic checking of user interfaces, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.2, p.124-167, April 2005
Eric Van Wyk, Specification languages in algebraic compilers, Theoretical Computer Science, v.291 n.3, p.351-385, 6 January 2003
S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
Hidetomo Machi , Kohji Tomita , Chiharu Hosono, The relative completeness of a version of CTL, Proceedings of the 2005 Australasian symposium on Theory of computing, p.81-85, January 01, 2005, Newcastle, Australia
R. F. Lutje Spelberg , W. J. Toetenel, Parametric real-time model checking using splitting trees, Nordic Journal of Computing, v.8 n.1, p.88-120, Spring 2001
Ansuman Banerjee , Pallab Dasgupta, The open family of temporal logics: Annotating temporal operators with input constraints, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.3, p.492-522, July 2005
Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994
Hyoung Seok Hong , Sung Deok Cha , Insup Lee , Oleg Sokolsky , Hasan Ural, Data flow testing as model checking, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Micah Lewis , Michael Jones, A dead variable analysis for explicit model checking, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
Orna Kupferman , Moshe Y. Vardi, From linear time to branching time, ACM Transactions on Computational Logic (TOCL), v.6 n.2, p.273-294, April 2005
Subash Shankar , Sinan Asa , Vladimir Sipos , Xiaowei Xu, Reasoning about real-time statecharts in the presence of semantic variations, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Foto Afrati , Theodore Andronikos , Vassia Pavlaki , Eugenie Foustoucos , Irène Guessarian, From CTL to datalog, Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday, p.72-85, June 08-08, 2003, San Diego, California, USA
R. H. Hardin , R. P. Kurshan , S. K. Shukla , M. Y. Vardi, A New Heuristic for Bad Cycle Detection Using BDDs, Formal Methods in System Design, v.18 n.2, p.131-140, March 1, 2001
Satoshi Yamane, Automatic effective verification method for distributed and concurrent systems using timed language inclusion, Engineering of distributed control systems, Nova Science Publishers, Inc., Commack, NY, 2001
Karen Yorav , Orna Grumberg, Static Analysis for State-Space Reductions Preserving Temporal Logics, Formal Methods in System Design, v.25 n.1, p.67-96, July 2004
Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, v.10 n.1, p.47-71, February 1997
Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003
Robert V. Rubin , James Walker, II , Eric J. Golin, Early Experience with the Visual Programmer's WorkBench, IEEE Transactions on Software Engineering, v.16 n.10, p.1107-1121, October 1990
Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Compiling Real-Time Specifications into Extended Automata, IEEE Transactions on Software Engineering, v.18 n.9, p.794-804, September 1992
Roberto Ziller , Klaus Schneider, Combining supervisor synthesis and model checking, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.331-362, May 2005
E. Jane Cameron , David M. Cohen , Timothy M. Guinther , William M. Keese, Jr. , Cynthia Norman , Hassan N. Srinidhi, The L.0 Language and Environment for Protocol Simulation and Prototyping, IEEE Transactions on Computers, v.40 n.4, p.562-571, April 1991
Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
María Alpuente , María del Mar Gallardo , Ernesto Pimentel , Alicia Villanueva, A semantic framework for the abstract model checking of tccp programs, Theoretical Computer Science, v.346 n.1, p.58-95, 23 November 2005
Thomas A. Henzinger , Orna Kupferman , Rupak Majumdar, On the universal and existential fragments of the μ-calculus, Theoretical Computer Science, v.354 n.2, p.173-186, 28 March 2006
Samik Basu , C. R. Ramakrishnan, Compositional analysis for verification of parameterized systems, Theoretical Computer Science, v.354 n.2, p.211-229, 28 March 2006
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Strong planning under partial observability, Artificial Intelligence, v.170 n.4, p.337-384, April 2006
Roberto Barbuti , Nicoletta Francesco , Antonella Santone , Gigliola Vaglini, Reduced Models for Efficient CCS Verification, Formal Methods in System Design, v.26 n.3, p.319-350, May 2005
Roderick Bloem , Harold N. Gabow , Fabio Somenzi, An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps, Formal Methods in System Design, v.28 n.1, p.37-56, January 2006
Felix Sheng-Ho Chang , Daniel Jackson, Symbolic model checking of declarative relational models, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite StateSpaces using QDDs, Formal Methods in System Design, v.14 n.3, p.237-255, May 1999
J. Billington , G. R. Wheeler , M. C. Wilbur-Ham, PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols, IEEE Transactions on Software Engineering, v.14 n.3, p.301-316, March 1988
María del Mar Gallardo , Jesús Martínez , Pedro Merino , Estefanía Rosales, Using XML to implement abstraction for Model Checking, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
Rance Cleaveland , S. Purushothaman Iyer , Murali Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theoretical Computer Science, v.342 n.2-3, p.316-350, 7 September 2005
Alexander Rabinovich , Philippe Schnoebelen, BTL2 and the expressive power of ECTL+, Information and Computation, v.204 n.7, p.1023-1044, July 2006
Lars Grunske, Specification patterns for probabilistic quality properties, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
Maurice H. ter Beek , Stefania Gnesi , Nora Koch , Franco Mazzanti, Formal verification of an automotive scenario in service-oriented computing, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
Wuttipong Ruanthong , Pornsiri Muenchaisri, Model checking for aspect-oriented software evolution, Proceedings of the 4th WSEAS International Conference on Software Engineering, Parallel & Distributed Systems, p.1-6, February 13-15, 2005, Salzburg, Austria
T. Kropf , J. Ruf, Using MTBDDs for Discrete Timed Symbolic Model Checking, Proceedings of the 1997 European conference on Design and Test, p.182, March 17-20, 1997
Farn Wang , Geng-Dian Huang , Fang Yu, TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering, IEEE Transactions on Software Engineering, v.32 n.7, p.510-526, July 2006
Shmuel S. Tyszberowicz, How to Implement a Safe Real-Time System: The OBSERV Implementationof the Production Cell Case Study, Real-Time Systems, v.15 n.1, p.61-90, July 1, 1998
E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States
E. A. Emerson , A. P. Sistla, Utilizing symmetry when model-checking under fairness assumptions: an automata-theoretic approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.4, p.617-638, July 1997
A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States
Jin Yang , Aloysius K. Mok , Farn Wang, Symbolic model checking for event-driven real-time systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.386-412, March 1997
Yoann Padioleau , René Rydhof Hansen , Julia L. Lawall , Gilles Muller, Semantic patches for documenting and automating collateral evolutions in Linux device drivers, Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systems, p.10-es, October 22-22, 2006, San Jose, California
Håkan L. S. Younes , Reid G. Simmons, Statistical probabilistic model checking with a focus on time-bounded properties, Information and Computation, v.204 n.9, p.1368-1409, September 2006
Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
Marsha Chechik , Arie Gurfinkel , Benet Devereux , Albert Lai , Steve Easterbrook, Data structures for symbolic multi-valued model-checking, Formal Methods in System Design, v.29 n.3, p.295-344, November 2006
Marcelo Cezar Pinto , Luciana Foss , José Carlos Merino Mombach , Leila Ribeiro, Modelling, property verification and behavioural equivalence of lactose operon regulation, Computers in Biology and Medicine, v.37 n.2, p.134-148, February, 2007
Marta Kwiatkowska, Quantitative verification: models, techniques and tools, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
Shriram Krishnamurthi , Kathi Fisler, Foundations of incremental aspect model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.2, p.7-es, April 2007
Alessio Lomuscio , Franco Raimondi, The complexity of model checking concurrent programs against CTLK specifications, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Marta Kwiatkowska , Gethin Norman , David Parker, Using probabilistic model checking in systems biology, ACM SIGMETRICS Performance Evaluation Review, v.35 n.4, March 2008
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, From molecular interactions to gates: a systematic approach, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Chitta Baral , Thomas Eiter , Marcus Bjäreland , Mutsumi Nakamura, Maintenance goals of agents in a dynamic environment: Formulation and policy construction, Artificial Intelligence, v.172 n.12-13, p.1429-1469, August, 2008
Laura Bozzelli, Complexity results on branching-time pushdown model checking, Theoretical Computer Science, v.379 n.1-2, p.286-297, June, 2007
George Spanoudakis , Christos Kloukinas , Kelly Androutsopoulos, Towards security monitoring patterns, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
Sascha Klüppelholz , Christel Baier, Symbolic Model Checking for Channel-based Component Connectors, Electronic Notes in Theoretical Computer Science (ENTCS), v.175 n.2, p.19-37, June, 2007
Hahnsang Kim , Thierry Turletti , Amar Bouali, EPspectra: a formal toolkit for developing DSP software applications, Theory and Practice of Logic Programming, v.6 n.4, p.451-481, July 2006
R. Mehmood , J. Crowcroft , S. Hand , S. Smith, Grid-Level Computing Needs Pervasive Debugging, Proceedings of the 6th IEEE/ACM International Workshop on Grid Computing, p.186-193, November 13-14, 2005
Walter Dosch , Pornsiri Muenchaisri , Wuttipong Ruanthong , Annette Stümpel, Model checking for input/output properties of a black-box model, Proceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology, p.120-127, April 02-04, 2007, Phuket, Thailand
Tomohiro Yoneda , Bernd--Holger Schlingloff, Efficient Verification of Parallel Real–Time Systems, Formal Methods in System Design, v.11 n.2, p.187-215, Aug. 1997
Girish Bhat , Rance Cleaveland , Gerald Lüttgen, A practical approach to implementing real-time semantics, Annals of Software Engineering, v.7 n.1-4, p.127-155, 1999
Mihalis Yannakakis , David Lee, An Efficient Algorithm for Minimizing Real-Time Transition Systems, Formal Methods in System Design, v.11 n.2, p.113-136, Aug. 1997
L. E. Pinzon , H.-M. Hanisch , M. A. Jafari , T. Boucher, A Comparative Study of Synthesis Methods for Discrete Event Controllers, Formal Methods in System Design, v.15 n.2, p.123-167, Sept. 1999
E. Allen Emerson, Automated formal methods: model checking and beyond, ACM SIGSOFT Software Engineering Notes, v.25 n.1, p.49, Jan 2000
Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
Patrick Cousot , Radhia Cousot, Refining Model Checking by Abstract Interpretation, Automated Software Engineering, v.6 n.1, p.69-95, January 1999
José C. Campos , Michael D. Harrison, Model Checking Interactor Specifications, Automated Software Engineering, v.8 n.3-4, p.275-310, August 2001
Myla Archer , Constance Heitmeyer , Elvinia Riccobene, Proving Invariants of I/O Automata with TAME, Automated Software Engineering, v.9 n.3, p.201-232, August 2002
S. Morasca , A. Morzenti , P. San Pietro, A Case Study on Applying a Tool for Automated System Analysis Based on Modular Specifications Written in TRIO, Automated Software Engineering, v.7 n.2, p.125-155, May 2000
Farn Wang , Chia-Tien Lo, Procedure-Level Verification of Real-time Concurrent Systems, Real-Time Systems, v.16 n.1, p.81-114, Jan. 1999
Nazanin Mansouri , Ranga Vemuri, Accounting for various register allocation schemes during post-synthesis verification of RTL designs, Proceedings of the conference on Design, automation and test in Europe, p.46-es, January 1999, Munich, Germany
Joseph Y. Halpern, Set-theoretic completeness for epistemic and conditional logic, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.1-27, 1999
Markus Stumptner , Franz Wotawa, A survey of intelligent debugging, AI Communications, v.11 n.1, p.35-51, January 1998
N. G. Martin , Shamkant B. Navathe , Rafi Ahmed, Dealing with Temporal Schema Anomalies in History Databases, Proceedings of the 13th International Conference on Very Large Data Bases, p.177-184, September 01-04, 1987
Harry C. Li , Shriram Krishnamurthi , Kathi Fisler, Modular Verification of Open Features Using Three-Valued Model Checking, Automated Software Engineering, v.12 n.3, p.349-382, July 2005
Magdalena Kacprzak , Wojciech Penczek, Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic1, Autonomous Agents and Multi-Agent Systems, v.11 n.1, p.69-89, July 2005
J. Frossl , T. Kropf, Verifying real-time properties of MOS-transistor circuits, Proceedings of the 1995 European conference on Design and Test, p.314, March 06-09, 1995
Abhik Roychoudhury , Tulika Mitra , S. R. Karri, Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol, Proceedings of the conference on Design, Automation and Test in Europe, p.10828, March 03-07, 2003
Cinzia Bernardeschi , Alessandro Fantechi , Stefania Gnesi , Salvatore Larosa , Giorgio Mongardi , Dario Romano, A Formal Verification Environment for Railway Signaling System Design, Formal Methods in System Design, v.12 n.2, p.139-161, March 1, 1998
Massimo Franceschet , Angelo Montanari , Maarten De Rijke, Model Checking for Combined Logics with an Application to Mobile Systems, Automated Software Engineering, v.11 n.3, p.289-321, June 2004
Pallab Dasgupta , Arindam Chakrabarti , P. P. Chakrabarti, Open Computation Tree Logic for Formal Verification of Modules, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.735, January 07-11, 2002
A. Lakas , G. S. Gordon , A. Chetwynd, Specification and Verification of Real-Time Properties Using LOTOS and SQTL, Proceedings of the 8th International Workshop on Software Specification and Design, p.75, March 22-23, 1996
P. Ciancarini , F. Franze` , C. Mascolo, A Coordination Model to Specify Systems Including Mobile Agents, Proceedings of the 9th international workshop on Software specification and design, p.96, April 16-18, 1998
Carlos Areces , Miguel Felder , Dan Hirsch , Daniel Yankelevich, Modal Logic as a Design Notation, Proceedings of the 9th international workshop on Software specification and design, p.150, April 16-18, 1998
Véronique Bruyère , Emmanuel Dall'olio , Jean-François Raskin, Durations and parametric model-checking in timed automata, ACM Transactions on Computational Logic (TOCL), v.9 n.2, p.1-23, March 2008
Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002
Peter Buchholz , Peter Kemper, Efficient Computation and Representation of Large Reachability Sets for Composed Automata, Discrete Event Dynamic Systems, v.12 n.3, p.265-286, July 2002
David M. Goldschlag, A Mechanization of Unity in PC-NQTHM-92, Journal of Automated Reasoning, v.23 n.3, p.445-498, November 1999
Marc-Michel Corsini , Antoine Rauzy, Toupie: The µ-calculus over Finite Domains as a Constraint Language, Journal of Automated Reasoning, v.19 n.2, p.143-171, October 1997
Abhik Roychoudhury , I. V. Ramakrishnan, Inductively Verifying Invariant Properties of Parameterized Systems, Automated Software Engineering, v.11 n.2, p.101-139, April 2004
A. Dovier , E. Quintarelli, Applying model-checking to solve queries on semistructured data, Computer Languages, Systems and Structures, v.35 n.2, p.143-172, July, 2009
Z. Manna , A. Pnueli, Specification and verification of concurrent programs by A∀automata, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-2, January 21-23, 1987, Munich, West Germany
Saikat Mukherjee , Srinath Srinivasa , Satish Chandra D, Validating for Liveness in Hidden Adversary Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.3, p.53-67, May, 2008
Christel Baier , Lucia Cloth , Boudewijn R. Haverkort , Matthias Kuntz , Markus Siegle, Model Checking Markov Chains with Actions and State Labels, IEEE Transactions on Software Engineering, v.33 n.4, p.209-224, April 2007
Arne Meier , Martin Mundhenk , Michael Thomas , Heribert Vollmer, The Complexity of Satisfiability for Fragments of CTL and CTL*;, Electronic Notes in Theoretical Computer Science (ENTCS), 223, p.201-213, December, 2008
Enrique Alba , Francisco Chicano, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Computers and Operations Research, v.35 n.10, p.3161-3183, October, 2008
A. Prasad Sistla , Min Zhou, Analysis of dynamic policies, Information and Computation, v.206 n.2-4, p.185-212, February, 2008
Nadjet Kamel , Yamine Ait Ameur , Sid Ahmed Selouani , Habib Hamam, A formal model to handle the adaptability of multimodal user interfaces, Proceedings of the 1st international conference on Ambient media and systems, p.1-7, February 11-14, 2008, Quebec, Canada
A. Prasad Sistla , V. N. Venkatakrishnan , Michelle Zhou , Hilary Branske, CMV: automatic verification of complete mediation for java virtual machines, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan
Marinella Petrocchi, Crypto-fraglets: networking, biology and security, Proceedings of the 1st international conference on Bio inspired models of network, information and computing systems, December 11-13, 2006, Cavalese, Italy
Yoann Padioleau , Julia Lawall , René Rydhof Hansen , Gilles Muller, Documenting and automating collateral evolutions in linux device drivers, ACM SIGOPS Operating Systems Review, v.42 n.4, May 2008
Tobias Nopper , Christoph Scholl , Bernd Becker, Computation of minimal counterexamples by using black box techniques and symbolic methods, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Marta Kwiatkowska, Quantitative verification: models techniques and tools, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Matteo Pradella , Angelo Morzenti , Pierluigi San Pietro, The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Sophie Laplante , Richard Lassaigne , Frédéric Magniez , Sylvain Peyronnet , Michel de Rougemont, Probabilistic abstraction for model checking: An approach based on property testing, ACM Transactions on Computational Logic (TOCL), v.8 n.4, p.20-es, August 2007
Mark R. Greenstreet , Suwen Yang, Verifying start-up conditions for a ring oscillator, Proceedings of the 18th ACM Great Lakes symposium on VLSI, May 04-06, 2008, Orlando, Florida, USA
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, Formal methods for the analysis and synthesis of nanometer-scale cellular arrays, ACM Journal on Emerging Technologies in Computing Systems (JETC), v.4 n.2, p.1-27, April 2008
Wojciech Jamroga , Thomas Ågotnes, Modular interpreted systems, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii
Emilie Balland , Pierre-Etienne Moreau , Antoine Reilles, Bytecode Rewriting in Tom, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.1, p.19-33, July, 2007
Mahmoud Askari , Hamid Shojaei , Fataneh Faghani, Symbolic counter-example generation for model checking, Proceedings of the 7th WSEAS International Conference on Application of Electrical Engineering, p.154-159, July 02-04, 2008, Trondheim, Norway
María del Mar Gallardo , Jesús Martínez , Pedro Merino , Ernesto Pimentel, On The Evolution Of Reliability Methods For Critical Software, Journal of Integrated Design & Process Science, v.10 n.4, p.55-67, December 2006
José C. Campos , Michael D. Harrison, Interaction engineering using the IVY tool, Proceedings of the 1st ACM SIGCHI symposium on Engineering interactive computing systems, July 15-17, 2009, Pittsburgh, PA, USA
Pablo Moreno-Ger , Rubén Fuentes-Fernández , José-Luis Sierra-Rodríguez , Baltasar Fernández-Manjón, Original papers: Model-checking for adventure videogames, Information and Software Technology, v.51 n.3, p.564-580, March, 2009
Alexander Rabinovich, Arity hierarchy for temporal logics, Theoretical Computer Science, v.403 n.2-3, p.373-381, August, 2008
Andrea Fedeli , Franco Fummi , Graziano Pravadelli, Properties Incompleteness Evaluation by Functional Verification, IEEE Transactions on Computers, v.56 n.4, p.528-544, April 2007
Praveen Tiwari , Raj S. Mitra, Hybrid Verification of Protocol Bridges, IEEE Design & Test, v.24 n.2, p.124-131, March 2007
Michele Sama , David S. Rosenblum , Zhimin Wang , Sebastian Elbaum, Model-based fault detection in context-aware adaptive applications, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
Ansuman Banerjee , Pallab Dasgupta , P. P. Chakrabarti, Auxiliary state machines + context-triggered properties in verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.4, p.1-31, September 2008
Qingwei Wu , Michael S. Hsiao, A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal, IEEE Transactions on Computers, v.55 n.11, p.1325-1334, November 2006
Jeremy Sproston , Susanna Donatelli, Backward Bisimulation in Markov Chain Model Checking, IEEE Transactions on Software Engineering, v.32 n.8, p.531-546, August 2006
Stijn Heymans , Davy Van Nieuwenborgh , Dirk Vermeir, Open answer set programming with guarded programs, ACM Transactions on Computational Logic (TOCL), v.9 n.4, p.1-53, August 2008
Mark Reith , Jianwei Niu , William H. Winsborough, Toward practical analysis for trust management policy, Proceedings of the 4th International Symposium on Information, Computer, and Communications Security, March 10-12, 2009, Sydney, Australia
Paolo Ballarini , Radu Mardare , Ivan Mura, Analysing Biochemical Oscillation through Probabilistic Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.1, p.3-19, February, 2009
Alastair F. Donaldson , Alice Miller, Automatic Symmetry Detection for Promela, Journal of Automated Reasoning, v.41 n.3-4, p.251-293, November 2008
Vitus S. W. Lam, A formalism for reasoning about UML activity diagrams, Nordic Journal of Computing, v.14 n.1, p.43-64, January 2007
P. Bellini , P. Nesi , D. Rogai, Expressing and organizing real-time specification patterns via temporal logics, Journal of Systems and Software, v.82 n.2, p.183-196, February, 2009
Marta Kwiatkowska , Gethin Norman , David Parker , Maria Grazia Vigliotti, Probabilistic Mobile Ambients, Theoretical Computer Science, v.410 n.12-13, p.1272-1303, March, 2009
Robert M. Hierons , Kirill Bogdanov , Jonathan P. Bowen , Rance Cleaveland , John Derrick , Jeremy Dick , Marian Gheorghe , Mark Harman , Kalpesh Kapoor , Paul Krause , Gerald Lüttgen , Anthony J. H. Simons , Sergiy Vilkomir , Martin R. Woodward , Hussein Zedan, Using formal specifications to support testing, ACM Computing Surveys (CSUR), v.41 n.2, p.1-76, February 2009
Zhi-Hong Tao , Hans Kleine Büning , Li-Fu Wang, Direct model checking matrix algorithm, Journal of Computer Science and Technology, v.21 n.6, p.944-949, November 2006
Jin-Cheon Na , Richard Furuta, Open paper: caT: adapting and updating the trellis hypertext model, The New Review of Hypermedia and Multimedia, v.12 n.2, p.217-246, December 2006
K. L. McMillan, Model checking, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
Patricia Bouyer, Model-checking Timed Temporal Logics, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.323-341, March, 2009
Alfonso E. Gerevini , Patrik Haslum , Derek Long , Alessandro Saetti , Yannis Dimopoulos, Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners, Artificial Intelligence, v.173 n.5-6, p.619-668, April, 2009
Nils Bulling , Wojciech Jamroga , Jürgen Dix, Reasoning about temporal properties of rational play, Annals of Mathematics and Artificial Intelligence, v.53 n.1-4, p.51-114, August 2008
Roopak Sinha , Partha S. Roop , Samik Basu, SoC design approach using convertibility verification, EURASIP Journal on Embedded Systems, 2008, p.1-19, January 2008
J. Julliand , P. -A. Masson , E. Oudot, Partitioned PLTL model-checking for refined transition systems, Information and Computation, v.207 n.6, p.681-698, June, 2009
Stavros Tripakis, Checking timed Büchi automata emptiness on simulation graphs, ACM Transactions on Computational Logic (TOCL), v.10 n.3, p.1-19, April 2009
Tomas Matousek , Pavel Jezek, DeSpec: Modeling the Windows Driver Environment11This work was partially supported by the Czech Academy of Sciences project 1ET400300504 and the Grant Agency of the Czech Republic project GD201/05/H014., Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.7, p.55-69, April, 2009
Sascha Klüppelholz , Christel Baier, Symbolic model checking for channel-based component connectors, Science of Computer Programming, v.74 n.9, p.688-701, July, 2009
Sascha Klüppelholz , Christel Baier, Symbolic model checking for channel-based component connectors, Science of Computer Programming, v.74 n.9, p.688-701, July, 2009
Nihal Pekergin , Sana Younès, CSRL model checking with closed-form bounding distributions, Proceedings of the 3rd International Conference on Performance Evaluation Methodologies and Tools, October 20-24, 2008, Athens, Greece
Sara Kalvala , Richard Warburton , David Lacey, Program transformations using temporal logic side conditions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.4, p.1-48, May 2009
Parosh Aziz Abdulla , Frédéric Haziza , Mats Kindahl, Model checking race-freeness, ACM SIGARCH Computer Architecture News, v.36 n.5, December 2008
Iván Martínez-Ortiz , José-Luis Sierra , Baltasar Fernández-Manjón , Alfredo Fernández-Valmayor, Language engineering techniques for the development of e-learning applications, Journal of Network and Computer Applications, v.32 n.5, p.1092-1105, September, 2009
Rune M. Jensen , Manuela M. Veloso, OBDD-based universal planning for synchronized agents in non-deterministic domains, Journal of Artificial Intelligence Research, v.13 n.1, p.189-226, August 2000
Orna Grumberg , Shlomi Livne , Shaul Markovitch, Learning to order BDD variables in verification, Journal of Artificial Intelligence Research, v.18 n.1, p.83-116, January 2003
Alessandro Cimatti , Marco Roveri, Conformant planning via symbolic model checking, Journal of Artificial Intelligence Research, v.13 n.1, p.305-338, August 2000
Moshe Y. Vardi, Automated verification: graphs, logic, and automata, Proceedings of the 18th international joint conference on Artificial intelligence, p.1603-1606, August 09-15, 2003, Acapulco, Mexico
Aditya Kanade , Amitabha Sanyal , Uday P. Khedker, Validation of GCC optimizers through trace generation, Software—Practice & Experience, v.39 n.6, p.611-639, April 2009
Ayaz Isazadeh , Jaber Karimpour, A new formalism for mathematical description and verification of component-based systems, The Journal of Supercomputing, v.49 n.3, p.334-353, September 2009

INDEX TERMS

Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES


General Terms:
Verification

Collaborative Colleagues:
E. M. Clarke: colleagues
E. A. Emerson: colleagues
A. P. Sistla: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player