Bibliography

1

Richard J. Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, and Jon D. Reese.
Model checking large software specifications.
In David Garlan, editor, Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 156-166, San Francisco, CA, USA, October 1996. ACM.
A full version to appear in IEEE Transactions on Software Engineering.

2

M. Benerecetti, F. Giunchiglia, and L. Serafini.
Model Checking Multiagent Systems.
Journal of Logic and Computation, Special Issue on Computational & Logical Aspects of Multi-Agent Systems, 8(3):401-423, 1998.
Also IRST-Technical Report 9708-07, IRST, Trento, Italy.

3

S. Berezin, S. Campos, and E. Clarke.
Compositional Reasoning in Model Checking.
Technical Report CMU-CS-98-106, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, February 1998.
To appear in proceedings of the COMPOS'97 workshop.

4

Armin Biere.
$\mu$cke - efficient $\mu$-calculus model checking.
In International Conference on Computer-Aided Verification, number 1254 in LNCS, pages 468-471. Springer, 1997.

5

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu.
Symbolic Model Checking without BDDs.
In Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), March 1999.
To appear.

6

R. K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz S., Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa.
VIS: A system for Verification and Synthesis.
In Rajeev Alur and Thomas A. Henzinger, editors, Proc. Computer Aided Verification (CAV'96), number 1102 in LNCS, New Brunswick, New Jersey, USA, July/August 1996. Springer-Verlag.

7

R. E. Bryant.
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Transactions on Computers, C-35(8):677-691, August 1986.

8

R. E. Bryant.
Symbolic Boolean manipolation with ordered binary-decision diagrams.
ACM Computing Surveys, 24(3):293-318, September 1992.

9

J. R. Burch, E. M. Clarke, and D. E. Long.
Representing Circuits More Efficiently in Symbolic Model Checking.
In Proceedings of the 28th ACM/IEEE Design Automation Conference, pages 403-407, Los Alamitos, CA, June 1991. IEEE Computer Society Press.

10

J. R. Burch, E. M. Clarke, and D. E. Long.
Symbolic model checking with partitioned transition relations.
In A. Halaas and P.B. Denyer, editors, International Conference on Very Large Scale Integration, pages 49-58, Edinburgh, Scotland, August 1991. IFIP Transactions, North-Holland.

11

J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill.
Symbolic Model Checking for Sequential Circuit Verification.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401-424, April 1994.

12

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang.
Symbolic Model Checking: 10²⁰ States and Beyond.
Information and Computation, 98(2):142-170, June 1992.

13

S. Campos, E. Clarke, and M. Minea.
The Verus Tool: A quantitative approach to the formal verification of real-time systems.
In Orna Grumberg, editor, Proc. Computer Aided Verification (CAV'97), number 1254 in LNCS, Haifa, Israel, June 1997. Springer-Verlag.

14

S. Campos, E. M. Clarke, W. Marrero, M. Minea, and H. Hiraishi.
Computing Quantitive Characteristics of Finite-State Real-Time Systems.
Technical Report CMU-CS-94-147, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, May 1994.

15

S. Campos and O. Grumberg.
Selective quantitative analysis and interval model checking: Verifying different facets of a system.
In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Verification CAV, volume 1102 of Lecture Notes in Computer Science, pages 257-268, New Brunswick, NJ, USA, July/August 1996. Springer Verlag.

16

R. J. Chassell and Richard Stallman.
Texinfo: the GNU documentation format, October 1996.

17

A. Cimatti, E. Giunchiglia, F. Giunchiglia, and P. Traverso.
Planning via Model Checking: A Decision Procedure for ${\cal AR}$.
In S. Steel and R. Alami, editors, Proceeding of the Fourth European Conference on Planning, number 1348 in Lecture Notes in Artificial Intelligence, pages 130-142, Toulouse, France, September 1997. Springer-Verlag.
Also ITC-IRST Technical Report 9705-02, ITC-IRST Trento, Italy.

18

A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso.
Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System.
In Proceedings of SAFECOMP'98 - Seventeenth International Conference on Computer Safety, Reliability and Security, Heidelberg, Germany, 1998.
Also IRST-Technical Report 9702-09, Trento, Italy. Presented at the Third SPIN Workshop, Twente University, Enschede, The Netherlands, April 1997.

19

A. Cimatti and M. Roveri.
NUSMV 1.0: User Manual.
Technical report, ITC-IRST, Trento, Italy, December 1998.

20

A. Cimatti, M. Roveri, and P. Traverso.
Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains.
In Proceeding of the Fifteenth National Conference on Artificial Intelligence (AAAI-98), Madison, Wisconsin, 1998. AAAI-Press.
Also IRST-Technical Report 9801-10, Trento, Italy.

21

A. Cimatti, M. Roveri, and P. Traverso.
Strong Planning in Non-Deterministic Domains via Model Checking.
In Proceeding of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98), Carnegie Mellon University, Pittsburgh, USA, June 1998. AAAI-Press.

22

E. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. Long, K.McMillan, and L. Ness.
Verification of the FUTUREBUS+ cache coherence protocol.
In 11th CHDL, 1993.

23

E. M. Clarke and E. A. Emerson.
Synthesis of synchronization skeletons for branching time tem poral logic.
In Logic of Programs: Workshop. Springer Verlag, May 1981.
Lecture Notes in Computer Science No. 131.

24

E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao.
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
In 32nd Design Automation Conference (DAC 95), pages 427-432, San Francisco, CA, USA, June 1995.

1

E. M. Clarke, M. Khaira, and X. Zhao.
Word Level Model Checking Avoiding the Pentium FDIV Error.
In 33rd Design Automation Conference (DAC'96), pages 645-648, New York, June 1996. Association for Computing Machinery.

26

E. M. Clarke, K. L. McMillan, S. Campos, and V. Hartonas-Garmhausen.
Symbolic model checking.
In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Verification CAV, volume 1102 of Lecture Notes in Computer Science, pages 419-422, New Brunswick, NJ, USA, July/August 1996. Springer Verlag.

27

E. M. Clarke and J. M. Wing.
Formal methods: State of the art and future directions.
ACM Computing Surveys, 28(4):626-643, December 1996.

28

E.M. Clarke, E.A. Emerson, and A.P. Sistla.
Automatic verification of finite-state concurrent systems using temporal logic specifications.
ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.

29

O. Coudert, C. Berthet, and J.C. Madre.
Verification of synchronous sequential machines using symbolic execution.
In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 365-373, Grenoble, France, June 1989. Springer-Verlag.

30

O. Coudert, J. C. Madre, and H. Touati.
TiGeR Version 1.0 User Guide.
Digital Paris Research Lab, December 1993.

31

D. L. Dill, A, J. Drexler, A. J. Hu, and C. H. Yang.
Protocol verification as a hardware design aid.
In International Conference on Computer Design, VLSI in Computers and Processors, pages 522-525, Los Alamitos, Ca., USA, October 1992. IEEE Computer Society Press.

32

O. Grumberg E. Clarke and K. Hamaguchi.
Another Look at LTL Model Checking.
Formal Methods in System Design, 10(1):57-71, February 1997.

33

E. Emerson, A. Mok, A. Sistla, and J. Srinivasan.
Quantitative Temporal Reasoning.
In Proc. Computer Aided Verification, LNCS. Springer-Verlag, 1990.

34

J.C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu.
CADP: A Protocol Validation and Verification Toolbox.
In R. Alur and T.A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (CAV'96), number 1102 in Lecture Notes in Computer Science, pages 437-440, New Brunswick, NJ, USA, August 1996. Springer-Verlag.

35

D. Geist and I. Beer.
Efficient model checking by automated ordering of transition relation partitions.
In D. L. Dill, editor, Proc. Computer Aided Verification (CAV'94), number 818 in LNCS, Stanford, California, USA, June 1994. Springer-Verlag.

36

F. Giunchiglia and R. Sebastiani.
Building decision procedures for modal logics from propositional decision procedures - the case study of modal K.
In Proc. of the 13th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, New Brunswick, NJ, USA, August 1996. Springer Verlag.
Also DIST-Technical Report 96-0037 and IRST-Technical Report 9601-02.

37

F. Giunchiglia and P. Traverso.
Planning as Model Checking.
In Susanne Biundo, editor, Proceeding of the Fifth European Conference on Planning, Lecture Notes in Artificial Intelligence, Durham, United Kingdom, September 1999. Springer-Verlag.

38

F. Giunchiglia and T. Walsh.
A Theory of Abstraction.
Artificial Intelligence, 57(2-3):323-390, 1992.
Also IRST-Technical Report 9001-14, IRST, Trento, Italy.

39

V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, and F. Giunchiglia.
Verification of a Safety-Critical Railway Interlocking System with Real-time Constraints.
In Proceedings of the 28th International Symposium on Fault-Tolerant Computing (FTCS-28), pages 458-463, Munich, Germany, June 1998. IEEE Computer Society Press.

2

Klaus Havelund and Natarajan Shankar.
Experiments in Theorem Proving and Model Checking for Protocol Verification.
In Marie-Claude Gaudel and Jim Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, pages 662-681. Springer-Verlag, March 1996.

41

G. J. Holzmann.
The model checker Spin.
IEEE Trans. on Software Engineering, 23(5):279-295, May 1997.
Special issue on Formal Methods in Software Practice.

42

IEEE.
System Application Program Interface (API) [C Language].
Information technology--Portable Operating System Interface (POSIX). IEEE Computer Society, 345 E. 47th St, New York, NY 10017, USA, 1990.

43

H. Iwashita, T. Nakata, and F. Hirose.
CTL model checking based on forward state traversal.
In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pages 82-87, Washington, November10-14 1996. IEEE Computer Society Press.

44

S. A. Kripke.
Semantical considerations on modal logic.
In Proc. A colloquium on Modal and Many-Valued Logics, Helsinki, 1962.

45

O. Lichtenstein and A. Pnueli.
Checking that finite state concurrent programs satisfy their linear specifications.
In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97-107. ACM, ACM, January 1985.

46

K. L. McMillan and J. Schwalbe.
Formal verification of the encore gigamax cache consistency protocol.
In Proceedings of the International Symposium on Shared Memory Multiprocessors, pages 242-251. (sponsored by Information Processing Society, Tokyo, Japan), 1991.

47

K.L. McMillan.
Symbolic Model Checking.
Kluwer Academic Publ., 1993.

48

In-Ho Moon, Jae-Young Jang, Gary D. Hacthtel, Fabio Somenzi, Jun Yuan, and Carl Pixley.
Approximate Reachability Don't Cares fo CTL Model Checking.
In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, San Jose, California, November8-12 1998. IEEE Computer Society Press.

49

C. Pixley.
A Computational Theory and Implementation of Sequential Hardware Equivalence.
In DIMACS Workshop on Computer Aided Verification '90, pages 293-320, Providence, RI, 1990.

50

S. T. Probst.
Chemical Process Safety and Operability Analysis using Symbolic Model Checking.
PhD thesis, Department of Chemical Engineering - Carnegie Mellon University, Pittsburgh, PA1523 USA, May 1996.

51

J. P. Queille and J. Sifakis.
Specification and verification of concurrent systems in CESAR.
In Proc. 5th Int'l Symp. on Programming, Lecture Notes in Computer Science, Vol. 137, pages 337-371. SV, Berlin/New York, 1982.

52

J.P. Queille.
Le systéme CESAR: Description, spécification et analyse des applications réparties.
Thesis, Uuniversité Scientifique et Médicale de Grenoble, June 1982.

53

R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton.
Efficient BDD algorithms for FSM synthesis and verification.
In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

54

K. Ravi and F. Somenzi.
High-density reachability analysis.
In International Conference on Computer Aided Design, pages 154-158, Los Alamitos, Ca., USA, November 1995. IEEE Computer Society Press.

55

Herbert Schildt, American National Standards Institute, International Organization for Standardization, International Electrotechnical Commission, and ISO/IEC JTC 1.
The annotated ANSI C standard: American National Standard for Programming Languages C: ANSIISO 9899-1990.
OsborneMcGraw-Hill, Berkeley, CA, USA, 1990.

56

E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. Sangiovanni-Vincentelli.
SIS: A system for sequential circuit synthesis.
Technical report, U.C. Berkeley, May 1992.

57

F. Somenzi.
CUDD: CU Decision Diagram package -- release 2.1.2.
Department of Electrical and Computer Engineering -- University of Colorado at Boulder, April 1997.

58

Walter F. Tichy.
RCS: A system for version control.
Software Practice and Experience, 15(7):637-654, July 1985.

3

H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli.
Implicit state enumeration of finite state machines using BDDs.
In Satoshi Sangiovanni-Vincentelli, Alberto; Goto, editor, Proceedings of the IEEE International Conference on Computer-Aided Design, pages 130-133, Santa Clara, CA, November 1990. IEEE Computer Society Press.

60

M. Y. Vardi and P. Wolper.
An automata-theoretic approach to automatic program verification.
In Symposium on Logic in Computer Science (LICS '86), pages 332-345, Washington, D.C., USA, June 1986. IEEE Computer Society Press.

61

K. Winter.
Model Checking for Abstract State Machines.
Journal of Universal Computer Science, 3(5):689-701, 1997.

62

Bwolen Yang, Reid Simmons, Randal E. Bryant, and David R. O'Hallaron.
Optimizing Symbolic Model Checking for Constraint-Rich Models.
In N. Halbwachs and D. Peled, editors, Eleventh Conference on Computer-Aided Verification (CAV'99), number 1633 in Lecture Notes in Computer Science, pages 328-340, Trento - Italy, July 1999. Springer.

63

J. Yuan, J. Shen, J. Abraham, and A. Aziz.
On combining formal and informal verification.
In Proceedings of the 9th International Conference on Computer Aided Verification CAV, volume 1254 of Lecture Notes in Computer Science, pages 376-387, 1997.