|
 ABSTRACT
We survey recent progress in software model checking.
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
|
Abadi, M. and Lamport, L. 1993. Composing specifications. ACM Trans. Prog. Lang. Syst. 15, 1, 73--132.
|
| |
2
|
Abadi, M. and Lamport, L. 1995. Conjoining specifications. ACM Trans. Prog. Lang. Syst. 17, 3, 507--534.
|
| |
3
|
Agerwala, T. and Misra, J. 1978. Assertion graphs for verifying and synthesizing programs. Tech. Rep. 83, University of Texas, Austin, TX.
|
| |
4
|
Alpern, B. and Schneider, F. 1987. Recognizing safety and liveness. Distributed Computing 3, 3, 117--126.
|
| |
5
|
Alur, R., Dang, T., and Ivančić, F. 2006. Counterexample-guided predicate abstraction of hybrid systems. Theoret. Comput. Sci. 354, 2, 250--271.
|
| |
6
|
Alur, R. and Henzinger, T. 1999. Reactive modules. Form. Meth. Syst. Des. 15, 1, 7--48.
|
| |
7
|
Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., and Tasiran, S. 1998. Mocha: Modularity in model checking. In CAV 98: Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 521--525.
|
| |
8
|
Alur, R., Itai, A., Kurshan, R., and Yannakakis, M. 1995. Timing verification by successive approximation. Inf. Comput. 118, 1, 142--157.
|
| |
9
|
Andersen, L. 1994. Program analysis and specialization for the c programming language. Ph.D. dissertation. DIKU, University of Copenhagen, Copenhagen.
|
| |
10
|
Apt, K. and Olderog, E.-R. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag, Berlin, Germany.
|
| |
11
|
Armando, A., Mantovani, J., and Platania, L. 2006. Bounded model checking of software using SMT solvers instead of SAT solvers. In Model Checking Software: SPIN Workshop. Lecture Notes in Computer Science, vol. 3925. Springer-Verlag, Berlin, Germany, 146--162.
|
| |
12
|
Babic, D. and Hu, A. 2008. Calyso: scalable and precise extended static checking. In ICSE 08: Proceedings of the International Conference on Software Engineering. ACM, 211--220.
|
| |
13
|
Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. 2005. Widening operators for weakly-relational numeric abstractions. In SAS 05: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 3672. Springer-Verlag, New York, 3--18.
|
| |
14
|
Bagnara, R., Hill, P. M., and Zaffanella, E. 2008. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Prog. 72, 1-2, 3--21.
|
| |
15
|
Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S. K., and Ustuner, A. 2006. Thorough static analysis of device drivers. EuroSys. 73--85.
|
| |
16
|
Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. K. 2001. Automatic predicate abstraction of C programs. In PLDI 01: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 203--213.
|
| |
17
|
Ball, T., Millstein, T. D., and Rajamani, S. K. 2005. Polymorphic predicate abstraction. ACM Trans. Prog. Lang. Syst. 27, 2, 314--343.
|
| |
18
|
Ball, T., Podelski, A., and Rajamani, S. K. 2001. Boolean and Cartesian abstractions for model checking C programs. In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, New York, 268--283.
|
| |
19
|
Ball, T., Podelski, A., and Rajamani, S. K. 2002. Relative completeness of abstraction refinement for software model checking. In TACAS 02: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, New York, 158--172.
|
| |
20
|
Ball, T. and Rajamani, S. 2002a. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09, Microsoft Research.
|
| |
21
|
Ball, T. and Rajamani, S. 2002b. The SLAM project: debugging system software via static analysis. In POPL 02: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 1--3.
|
| |
22
|
Ball, T. and Rajamani, S. K. 2000a. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: Proceedings of the SPIN Workshop. Lecture Notes in Computer Science 1885. Springer-Verlag, 113--130.
|
| |
23
|
Ball, T. and Rajamani, S. K. 2000b. Boolean programs: a model and process for software analysis. Tech. Rep. MSR Technical Report 2000-14, Microsoft Research.
|
| |
24
|
Beckman, N., Nori, A. V., Rajamani, S. K., and Simmons, R. J. 2008. Proofs from tests. In ISSTA 08: Proceedings of the International Symposium on Software Testing and Analysis. ACM, New York, 3--14.
|
| |
25
|
Beyer, D., Chlipala, A. J., Henzinger, T. A., Jhala, R., and Majumdar, R. 2004. Generating tests from counterexamples. In ICSE 04: Proceedings of the International Conference on Software Engineering. ACM, New York, 326--335.
|
| |
26
|
Beyer, D., Henzinger, T., Majumdar, R., and Rybalchenko, A. 2007a. Invariant synthesis in combination theories. In VMCAI 07: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349. Springer-Verlag, Berlin, Germany, 378--394.
|
| |
27
|
Beyer, D., Henzinger, T., Majumdar, R., and Rybalchenko, A. 2007b. Path invariants. In PLDI 07: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 300--309.
|
| |
28
|
Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. 2007c. The software model checker blast. Softw. Tools Tech. Trans. 9, 5-6, 505--525.
|
| |
29
|
Beyer, D., Henzinger, T. A., and Théoduloz, G. 2007. Configurable software verification: Concretizing the convergence of model checking and program analysis. In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 504--518.
|
| |
30
|
Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., and Zhu, Y. 1999. Symbolic model checking using SAT procedures instead of BDDs. In DAC 99: Proceedings of the Design Automation Conference. ACM, New York, 317--320.
|
| |
31
|
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation, Complexity, Analysis, Transformation: Essays Dedicated to Neil D. Jones. Lecture Notes in Computer Science, vol. 2566. Springer-Verlag, Berlin, Germany, 85--108.
|
| |
32
|
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. 2003. A static analyzer for large safety-critical software. In PLDI 03: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 196--207.
|
| |
33
|
Bouajjani, A., Esparza, J., and Maler, O. 1994. Reachability analysis of pushdown automata: application to model checking. In CONCUR 97: Proceedings of the Symposium on Concurrency Theory. Lecture Notes in Computer Science, vol. 1243. Springer-Verlag, Berlin, Germany, 135--150.
|
| |
34
|
Bouajjani, A., Esparza, J., and Touili, T. 2003. A generic approach to the static analysis of concurrent programs with procedures. In POPL 03: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 62--73.
|
| |
35
|
Bouajjani, A., Fernandez, J.-C., and Halbwachs, N. 1990. Minimal model generation. In CAV 90: Proceedings of the Symposium on Computer-aided Verification. Lecture Notes in Computer Science, vol. 531. Springer-Verlag, Berlin, Germany, 197--203.
|
| |
36
|
Bradley, A., Manna, Z., and Sipma, H. 2005. The polyranking principle. In ICALP 05: Proceedings of the International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 3580. Springer-Verlag, Berlin, Germany, 1349--1361.
|
| |
37
|
Brat, G., Drusinsky, D., Giannakopolou, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Venet, A., Washington, R., and Visser, W. 2004. Experimental evaluation of verification and validation tools on Martian rover software. Form. Meth. Syst. Des. 25.
|
| |
38
|
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., and Sebastiani, R. 2008. The MathSAT 4 SMT solver. In CAV 08: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 299--303.
|
| |
39
|
Bryant, R. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35, 8, 677--691.
|
| |
40
|
Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 1992. Symbolic model checking: 1020 states and beyond. Inf. Comput. 98, 2, 142--170.
|
| |
41
|
Bustan, D. and Grumberg, O. 2003. Simulation-based minimization. ACM Trans. Comput. Logic 4, 181--206.
|
| |
42
|
Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., and Engler, D. 2006. EXE: automatically generating inputs of death. In CCS 02: Proceedings of the Conference on Computer and Communications Security. ACM, New York.
|
| |
43
|
Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., and Yorav, K. 2004. Efficient verification of sequential and concurrent C programs. Form. Meth. Syst. Des. 25, 2-3, 129--166.
|
| |
44
|
Chaki, S., Clarke, E., Kidd, N., Reps, T., and Touili, T. 2006. Verifying concurrent message-passing C programs with recursive calls. In TACAS 06: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3920. Springer-Verlag, Berlin, Germany, 334--349.
|
| |
45
|
Chaki, S., Clarke, E. M., Groce, A., and Strichman, O. 2003. Predicate abstraction with minimum predicates. In CHARME. 19--34.
|
| |
46
|
Chandra, S., Godefroid, P., and Palm, C. 2002. Software model checking in practice: an industrial case study. In ICSE 02: Proceedings of the International Conference on Software Engineering. ACM, New York, 431--441.
|
| |
47
|
Chang, B. E. and Rival, X. 2008. Relational inductive shape analysis. In POPL 08: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 247--260.
|
| |
48
|
Chase, D., Wegman, M., and Zadeck, F. 1990. Analysis of pointers and structures. In PLDI 90: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 296--310.
|
| |
49
|
Chaudhuri, S. 2008. Sub-cubic algorithms for recursive state machines. In POPL 08: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 159--169.
|
| |
50
|
Chen, H. and Wagner, D. 2002. MOPS: an infrastructure for examining security properties of software. In Proceedings of the ACM Conference on Computer and Communications Security 2002. 235--244.
|
| |
51
|
Clarke, E. M. and Emerson, E. A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, Berlin, Germany, 52--71.
|
| |
52
|
Clarke, E. M., Filkorn, T., and Jha, S. 1993. Exploiting symmetry in temporal logic model checking. In CAV 93: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Berlin, Germany, 450--462.
|
| |
53
|
Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, Berlin, Germany, 154--169.
|
| |
54
|
Clarke, E. M., Grumberg, O., and Long, D. 1992. Model checking and abstraction. In POPL 92: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 343--354.
|
| |
55
|
Clarke, L. 1976. A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 2, 215--222.
|
| |
56
|
Colón, M. and Sipma, H. 2001. Synthesis of linear ranking functions. In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, Berlin, Germany, 67--81.
|
| |
57
|
Colón, M. and Sipma, H. 2002. Practical methods for proving program termination. In CAV 02: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 442--454.
|
| |
58
|
Constable, R. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ.
|
| |
59
|
Cook, B., Podelski, A., and Rybalchenko, A. 2006. Termination proofs for systems code. In PLDI 06: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 415--426.
|
| |
60
|
Cook, S. A. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70--90.
|
| |
61
|
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In ICSE 00: Proceedings of the International Conference on Software Engineering. 439--448.
|
| |
62
|
Courcoubetis, C., Vardi, M., Wolper, P., and Yannakakis, M. 1992. Memory-efficient algorithms for the verification of temporal properties. Form. Meth. Syst. Des. 1, 275--288.
|
| |
63
|
Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In ISOP. 106--130.
|
| |
64
|
Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for the static analysis of programs. In POPL 77: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 238--252.
|
| |
65
|
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In POPL 79: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 269--282.
|
| |
66
|
Cousot, P. and Cousot, R. 2000. Temporal abstract interpretation. In POPL 00: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 12--25.
|
| |
67
|
Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear restraints among variables of a program. In POPL 78: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York.
|
| |
68
|
Craig, W. 1957. Linear reasoning. J. Symbol. Logic 22, 250--268.
|
| |
69
|
Das, M., Lerner, S., and Seigle, M. 2002. ESP: Path-sensitive program verification in polynomial time. In PLDI 02: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 57--68.
|
| |
70
|
Das, S., Dill, D. L., and Park, S. 1999. Experience with predicate abstraction. In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Berlin, Germany, 160--171.
|
| |
71
|
de Millo, R., Lipton, R., and Perlis, A. 1979. Social processes and proofs of theorems and programs. Commun. ACM 22, 271--280.
|
| |
72
|
de Moura, L. and Bjørner, N. 2008. Z3: An efficient SMT solver. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 337--340.
|
| |
73
|
de Moura, L. and Ruess, H. 2003. Bounded model checking and induction: From refutation to verification. In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 14--26.
|
| |
74
|
de Moura, L., Ruess, H., and Sorea, M. 2002. Lazy theorem proving for bounded model checking over infinite domains. In CADE 02: Proceedings of the Symposium on Automated Deduction. Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, Berlin, Germany, 438--455.
|
| |
75
|
Dijkstra, E. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.
|
| |
76
|
Dill, D. 1996. The Murphi verification system. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 390--393.
|
| |
77
|
Dimitrova, R. and Podelski, A. 2008. Is lazy abstraction a decision procedure for broadcast protocols? In VMCAI 08: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4905. Springer-Verlag, Berlin, Germany, 98--111.
|
| |
78
|
Distefano, D., O'Hearn, P. W., and Yang, H. 2006. A local shape analysis based on separation logic. In TACAS 06: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3920. Springer-Verlag, Berlin, Germany, 287--302.
|
| |
79
|
Doner, J. E. 1965. Decidability of the weak second-order theory of two successors. Notices Amer. Math. Soc. 12, 365--468.
|
| |
80
|
Duterte, B. and de Moura, L. 2006. A fast linear-arithmetic solver for DPLL(T). In CAV 06: Proceedings of the International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, Berlin, Germany, 81--94.
|
| |
81
|
Dwyer, M. and Clarke, L. 1994. Data flow analysis for verifying properties of concurrent programs. In FSE 94: Proceedings of the Symposium on Foundations of Software Engineering. ACM, New York, 62--75.
|
| |
82
|
Edelkamp, S., Leue, S., and Lluch-Lafuente, A. 2004. Directed explicit-state model checking in the validation of communication protocols. Softw. Tools Tech. Trans. 5, 247--267.
|
| |
83
|
Een, N. and Sorensson, N. 2003. An extensible SAT solver. In SAT 2003: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, vol. 2919. Springer-Verlag, Berlin, Germany, 502--518.
|
| |
84
|
Emerson, E. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. vol. B. Elsevier Science Publishers, Amsterdam, the Netherlands, 995--1072.
|
| |
85
|
Emerson, E. and Lei, C. 1986. Efficient model checking in fragments of the propositional μ-calculus. In Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 267--278.
|
| |
86
|
Emerson, E. and Sistla, A. 1996. Symmetry and model checking. Form. Meth. Syst. Des. 9, 105--131.
|
| |
87
|
Esparza, J. and Schwoon, S. 2001. A BDD-based model checker for recursive programs. In CAV. 324--336.
|
| |
88
|
Fahndrich, M. and DeLine, R. 2004. Typestates for objects. In ECOOP 04: Proceedings of the Symposium on Object-Oriented Programming. Lecture Notes in Computer Science, vol. 3086. Springer-Verlag, Berlin, Germany, 465--490.
|
| |
89
|
Fischer, J., Jhala, R. and Majumdar, R. 2005. Joining dataflow with predicates. In ESEC/FSE 2005: Proceedings of the Symposium on Foundations of Software Engineering. ACM, New York, 227--236.
|
| |
90
|
Flanagan, C. 2006. Hybrid type checking. In POPL 06: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York.
|
| |
91
|
Flanagan, C., Freund, S. and Qadeer, S. 2002. Thread-modular verification for shared-memory programs. In ESOP 02: Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, Berlin, Germany, 262--277.
|
| |
92
|
Flanagan, C., Freund, S., Qadeer, S., and Seshia, S. 2005. Modular verification of multithreaded programs. Theoret. Comput. Sci. 338, 153--183.
|
| |
93
|
Flanagan, C., Joshi, R., and Leino, K. R. M. 2001. Annotation inference for modular checkers. Inf. Proc. Lett. 77, 2-4, 97--108.
|
| |
94
|
Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In PLDI 02: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 234--245.
|
| |
95
|
Flanagan, C. and Qadeer, S. 2002. Predicate abstraction for software verification. In POPL 02: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 191--202.
|
| |
96
|
Flanagan, C. and Saxe, J. 2000. Avoiding exponential explosion: generating compact verification conditions. In POPL 00: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 193--205.
|
| |
97
|
Floyd, R. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science. American Mathematical Society, 19--32.
|
| |
98
|
Foster, J., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In PLDI 02: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 1--12.
|
| |
99
|
Francez, N. 1986. Fairness. Springer-Verlag, Berlin, Germany.
|
| |
100
|
Fraser, R., Kamhi, G., Ziv, B., Vardi, M., and Fix, L. 2000. Prioritized traversal: efficient reachability analysis for verification and falsification. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, Berlin, Germany, 389--402.
|
| |
101
|
Ganai, M. and Gupta, A. 2006. Accelerating high-level bounded model checking. In ICCAD 06: Proceedings of the International Conference on Computer-Aided Design. ACM, New York, 794--801.
|
| |
102
|
Ghiya, R. and Hendren, L. J. 1996. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In POPL 96: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 1--15.
|
| |
103
|
Giesl, J. and Kapur, D. 2001. Decidable classes of inductive theorems. In IJCAR 2001: Proceedings of the International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 2083. Springer-Verlag, Berlin, Germany, 469--484.
|
| |
104
|
Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, Berlin, Germany.
|
| |
105
|
Godefroid, P. 1997. Model checking for programming languages using Verisoft. In POPL 97: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 174--186.
|
| |
106
|
Godefroid, P., Klarlund, N., and Sen, K. 2005. DART: Directed Automated Random Testing. In PLDI 05: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 213--223.
|
| |
107
|
Gopan, D., Reps, T. W., and Sagiv, S. 2005. A framework for numeric analysis of array operations. In POPL 05: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 338--350.
|
| |
108
|
Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In CAV. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 72--83.
|
| |
109
|
Gulavani, B. S., Chakraborty, S., Nori, A. V., and Rajamani, S. K. 2008. Automatically refining abstract interpretations. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 443--458.
|
| |
110
|
Gulavani, B. S., Henzinger, T. A., Kannan, Y., Nori, A. V., and Rajamani, S. K. 2006. Synergy: A new algorithm for property checking. In FSE 06: Proceedings of the Symposium on Foundations of Software Engineering. ACM, New York, 117--127.
|
| |
111
|
Gulwani, S., McCloskey, B., and Tiwari, A. 2008. Lifting abstract interpreters to quantified logical domains. In POPL 08: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 235--246.
|
| |
112
|
Gulwani, S. and Tiwari, A. 2006. Combining abstract interpreters. In PLDI 2006: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 376--386.
|
| |
113
|
Gupta, A., Henzinger, T., Majumdar, R., Rybalchenko, A., and Xu, R. 2008. Proving non-termination. In POPL 08: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 147--158.
|
| |
114
|
Gupta, A., Majumdar, R., and Rybalchenko, A. 2009. From tests to proofs. In TACAS 09: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 5505. Springer-Verlag, Berlin, Germany, 262--276.
|
| |
115
|
Hackett, B. and Aiken, A. 2006. How is aliasing used in systems software? In FSE 06: Proceedings of the Symposium on Foundations of Software Engineering. ACM, New York, 69--80.
|
| |
116
|
Hardekopf, B. and Lin, C. 2007. The ant and the grasshopper: Fast and accurate pointer analysis for millions of lines of code. In PLDI 07: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 290--299.
|
| |
117
|
Hart, P., Nilsson, N., and Raphael, B. 1968. A formal basis for the heuristic determination of minimum cost paths. IEEE Trans. Syst. Sci. Cybernetics SSC4 2, 100--107.
|
| |
118
|
Havelund, K. and Pressburger, T. 2000. Model checking Java programs using Java Pathfinder. Softw. Tools Tech. Trans. (STTT) 2, 4, 72--84.
|
| |
119
|
Henzinger, T., Jhala, R., Majumdar, R., and McMillan, K. 2004. Abstractions from proofs. In POPL 04: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 232--244.
|
| |
120
|
Henzinger, T., Jhala, R., Majumdar, R., and Qadeer, S. 2003. Thread-modular abstraction refinement. In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany.
|
| |
121
|
Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In POPL 02: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 58--70.
|
| |
122
|
Henzinger, T., Qadeer, S., and Rajamani, S. 1998. You assume, we guarantee: methodology and case studies. In CAV 98: Proceedings of the Symposium on Computer-Aided Verification, Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 440--451.
|
| |
123
|
Henzinger, T. A., Jhala, R., and Majumdar, R. 2004. Race checking by context inference. In PLDI 2004: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 1--12.
|
| |
124
|
Hind, M. 2001. Pointer analysis: Haven't we solved this problem yet? In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE'01). ACM, New York, 54--61.
|
| |
125
|
Hoare, C. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 576--580.
|
| |
126
|
Holzmann, G. 1997. The Spin model checker. IEEE Trans. Softw. Eng. 23, 5 (May), 279--295.
|
| |
127
|
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004. The boundary between decidability and undecidability for transitive-closure logics. In CSL. 160--174.
|
| |
128
|
Ip, C. and Dill, D. 1996. Better verification through symmetry. Form. Meth. Syst. Des. 9, 41--75.
|
| |
129
|
Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., and Ashar, P. 2008. Efficient SAT-based bounded model checking for software verification. Theoret. Comput. Sci. 404, 3, 256--274.
|
| |
130
|
Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., Shlyakhter, I., and Ashar, P. 2005. F-soft: Software verification platform. In CAV 05: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 301--306.
|
| |
131
|
Jain, H., Ivančić, F., Gupta, A., Shlyakhter, I., and Wang, C. 2006. Using statically computed invariants inside the predicate abstraction and refinement loop. In CAV 06: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 137--151.
|
| |
132
|
Jha, S. K., Krogh, B. H., Weimer, J. E., and Clarke, E. M. 2007. Reachability for linear hybrid automata using iterative relaxation abstraction. In Proceedings of the 12th ACM International Conference on Hybrid Systems: Computation and Control. ACM, New York, 287--300.
|
| |
133
|
Jhala, R. and Majumdar, R. 2005. Path slicing. In PLDI 05: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 38--47.
|
| |
134
|
Jhala, R. and McMillan, K. 2006. A practical and complete approach to predicate refinement. In TACAS 06: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2987. Springer-Verlag, Berlin, Germany, 298--312.
|
| |
135
|
Jhala, R. and McMillan, K. L. 2005. Interpolant-based transition relation approximation. In CAV 05: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 39--51.
|
| |
136
|
Jones, C. 1983. Tentative steps toward a development method for interfering programs. ACM Trans. Programming Languages Systems 5, 4, 596--619.
|
| |
137
|
Kahlon, V. and Gupta, A. 2007. On the analysis of interacting pushdown systems. In POPL 07: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 303--314.
|
| |
138
|
Katz, S. and Peled, D. 1992. Verification of distributed programs using representative interleaving sequences. Distrib. Comput. 6, 2, 107--120.
|
| |
139
|
Killian, C. E., Anderson, J. W., Jhala, R., and Vahdat, A. 2007. Life, death, and the critical transition: Finding liveness bugs in systems code (awarded best paper). In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI). ACM, New York, 243--256.
|
| |
140
|
King, J. 1976. Symbolic execution and program testing. Commun. ACM 19, 7, 385--394.
|
| |
141
|
Korf, R. 1985. Depth-first iterative deepening: an optimal admissible tree search. Artif. Intell. 27, 97--109.
|
| |
142
|
Kroening, D., Clarke, E., and Yorav, K. 2003. Behavioral consistency of C and Verilog programs using bounded model checking. In DAC 03: Proceedings of the Symposium on Design Automation Conference. ACM, New York, 368--371.
|
| |
143
|
Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ.
|
| |
144
|
Lahiri, S. K. and Bryant, R. E. 2004. Constructing quantified invariants via predicate abstraction. In Proceedings of the 5th International Conference on Verification Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 267--281.
|
| |
145
|
Lahiri, S. K. and Qadeer, S. 2008. Back to the future: revisiting precise program verification using SMT solvers. In POPL 08: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 171--182.
|
| |
146
|
Lal, A., Touili, T., Kidd, N., and Reps, T. W. 2008. Interprocedural analysis of concurrent programs under a context bound. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 282--298.
|
| |
147
|
Lamport, L. 1983. Specifying concurrent program modules. ACM Trans. Prog. Lang. Syst. 5, 2, 190--222.
|
| |
148
|
Lee, D. and Yannakakis, M. 1992. Online minimization of transition systems. In Proceedings of the 24th Annual Symposium on Theory of Computing. ACM, New York, 264--274.
|
| |
149
|
Lehmann, D., Pnueli, A., and Stavi, J. 1982. Impartiality, justice, and fairness: The ethics of concurrent termination. In ICALP 81: Proceedings of the International Conference on Automata, Languages, and Programming. Lecture Notes in Computer Science 115. Springer-Verlag, Berlin, Germany, 264--277.
|
| |
150
|
Leino, K. R. M. and Nelson, G. 1998. An extended static checker for Modula-3. In CC 98: Proceedings of the Symposium on Compiler Construction. Lecture Notes in Computer Science, vol. 1383. Springer-Verlag, Berlin, Germany, 302--305.
|
| |
151
|
Lev-Ami, T. and Sagiv, S. 2000. TVLA: A system for implementing static analyses. In Proceedings of the 5th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 1824. Springer-Verlag, Berlin, Germany, 280--301.
|
| |
152
|
Lluch-Lafuente, A. 2003. Directed search for the verification of communication protocols. Ph.D. dissertation, Univ., Freiburg, Freiburg, Germany.
|
| |
153
|
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., and Bensalem, S. 1995. Property-preserving abstractions for the verification of concurrent systems. Form. Meth. Syst. Des. 6, 11--44.
|
| |
154
|
Magill, S., Berdine, J., Clarke, E. M., and Cook, B. 2007. Arithmetic strengthening for shape analysis. In Proceedings of the 14th International Symposium on Static Analysis. Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany, 419--436.
|
| |
155
|
Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, Germany.
|
| |
156
|
Martin-Löf, P. 1984. Constructive mathematics and computer programming. Roy. Soc. London Philos. Trans. Ser. A 312, 501--518.
|
| |
157
|
McMillan, K. 1993. Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic Publishers.
|
| |
158
|
McMillan, K. L. 2004. An interpolating theorem prover. In TACAS: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 16--30.
|
| |
159
|
McMillan, K. L. 2006. Lazy abstraction with interpolants. In CAV 2006: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 123--136.
|
| |
160
|
McMillan, K. L. 2008. Quantified invariant generation using an interpolating saturation prover. In Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 413--427.
|
| |
161
|
Meyer, R., Faber, J., and Rybalchenko, A. 2006. Model checking duration calculus: A practical approach. In ICTAC 06: Proceedings of the 3rd International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science, vol. 4281. Springer-Verlag, Berlin, Germany, 332--346.
|
| |
162
|
Miné, A. 2006. The octagon abstract domain. Higher-Order Symb. Comput. 19, 1, 31--100.
|
| |
163
|
Misra, J. and Chandy, K. 1981. Proofs of networks of processes. IEEE Trans. Softw. Eng. SE-7, 4, 417--426.
|
| |
164
|
Møller, A. and Schwartzbach, M. I. 2001. The Pointer assertion logic engine. In PLDI: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 221--231.
|
| |
165
|
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In DAC 01: Proceedings of the Design Automation Conference. ACM, New York, 530--535.
|
| |
166
|
Muchnick, S. 1997. Advanced Compiler Design and Implementation. Morgan-Kaufman, San Francisco, CA.
|
| |
167
|
Musuvathi, M. and Engler, D. R. 2004. Model checking large network protocol implementations. In NSDI. 155--168.
|
| |
168
|
Musuvathi, M. and Qadeer, S. 2007. Iterative context bounding for systematic testing of multithreaded programs. In PLDI: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 446--455.
|
| |
169
|
Namjoshi, K. S. and Kurshan, R. P. 2000. Syntactic program transformations for automatic abstraction. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 435--449.
|
| |
170
|
Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., and Birkedal, L. 2008. Ynot: Reasoning with the awkward squad. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP. ACM, New York.
|
| |
171
|
Necula, G. C. and Lee, P. 2000. Proof generation in the Touchstone theorem prover. In CADE 00: Proceedings of the Symposium on Computer-Aided Deduction. Lecture Notes in Computer Science, vol. 1831. Springer-Verlag, Berlin, Germany, 25--44.
|
| |
172
|
Nelson, G. 1981. Techniques for program verification. Tech. Rep. CSL81-10, Xerox Palo Alto Research Center, Palo Alto, CA.
|
| |
173
|
Nelson, G. 1983. Verifying reachability invariants of linked structures. In POPL 83: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 38--47.
|
| |
174
|
Nelson, G. and Oppen, D. 1980. Fast decision procedures based on congruence closure. J. ACM 27, 2, 356--364.
|
| |
175
|
Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. 1996. PVS: Combining specification, proof checking, and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 411--414.
|
| |
176
|
Pasareanu, C. S., Giannakopoulou, D., Bobaru, M. G., Cobleigh, J. M. and Barringer, H. 2008. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form. Meth. Syst. Des. 32, 3, 175--205.
|
| |
177
|
Penix, J., Visser, W., Park, S., Pasareanu, C., Engstrom, E., Larson, A., and Weininger, N. 2005. Verifying time partitioning in the DEOS scheduling kernel. Form. Meth. Syst. Des. 26.
|
| |
178
|
Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 46--57.
|
| |
179
|
Pnueli, A., Podelski, A., and Rybalchenko, A. 2005. Separating fairness and well-foundedness for the analysis of fair discrete systems. In TACAS 05: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3440. Springer-Verlag, Berlin, Germany, 124--139.
|
| |
180
|
Podelski, A. and Rybalchenko, A. 2004a. A complete method for the synthesis of linear ranking functions. In VMCAI. 239--251.
|
| |
181
|
Podelski, A. and Rybalchenko, A. 2004b. Transition invariants. In LICS 04: Proceedings of the Symposium on Logic in Computer Science. IEEE, Computer Society Press, Los Alamitos, CA.
|
| |
182
|
Podelski, A. and Rybalchenko, A. 2007. Armc: The logical choice for software model checking with abstraction refinement. In PADL 07: Proceedings of the Symposium on Practical Aspects of Declarative Programming. Lecture Notes in Computer Science, vol. 4354. Springer-Verlag, Berlin, Germany, 245--259.
|
| |
183
|
Podelski, A. and Wies, T. 2005. Boolean Heaps. In SAS: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 267--282.
|
| |
184
|
Qadeer, S., Rajamani, S. K., and Rehof, J. 2004. Summarizing procedures in concurrent programs. In POPL 04: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 245--255.
|
| |
185
|
Qadeer, S. and Rehof, J. 2005. Context-bounded model checking of concurrent software. In TACAS: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 93--107.
|
| |
186
|
Qadeer, S. and Wu, D. 2004. Kiss: Keep It Simple and Sequential. In PLDI: Proceedings of the Symposium on Programming Languages Design and Implementation. ACM, New York, 14--24.
|
| |
187
|
Queille, J. and Sifakis, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming, M. Dezani-Ciancaglini and U. Montanari, Eds. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, Berlin, Germany, 337--351.
|
| |
188
|
Ramalingam, G. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Prog. Lang. Syst. 22, 2, 416--430.
|
| |
189
|
Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 49--61.
|
| |
190
|
Reps, T. W., Schwoon, S., Jha, S., and Melski, D. 2005. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Prog. 58, 1-2, 206--263.
|
| |
191
|
Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 55--74.
|
| |
192
|
Rondon, P., Kawaguchi, M., and Jhala, R. 2008. Liquid types. In PLDI: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 158--169.
|
| |
193
|
Russell, S. and Norvig, P. 2003. Artificial Intelligence: A Modern Approach, 2nd ed. Prentice-Hall, Englewood Cliffs, NJ.
|
| |
194
|
Rybalchenko, A. and Sofronie-Stokkermans, V. 2007. Constraint solving for interpolation. In VMCAI. 346--362.
|
| |
195
|
Sagiv, S., Reps, T. W., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst. 24, 3, 217--298.
|
| |
196
|
Saidi, H. 2000. Model checking guided abstraction and analysis. In SAS 00: Proceedings of the Static-Analysis Symposium. Lecture Notes in Computer Science, vol. 1824, Springer-Verlag, Berlin, Germany, 377--396.
|
| |
197
|
Saïdi, H. and Shankar, N. 1999. Abstract and model check while you prove. In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Berlin, Germany, 443--454.
|
| |
198
|
Sankaranarayanan, S., Sipma, H. B., and Manna, Z. 2005. Scalable analysis of linear systems using mathematical programming. In VMCAI. 25--41.
|
| |
199
|
Schmidt, D. 1998. Data flow analysis is model checking of abstract interpretation. In POPL 98: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 38--48.
|
| |
200
|
Schmidt, D. A. and Steffen, B. 1998. Program analysis as model checking of abstract interpretations. In SAS 98: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 1503. Springer-Verlag, ACM, New York, 351--380.
|
| |
201
|
Sen, K., Marinov, D., and Agha, G. 2005. CUTE: A concolic unit testing engine for C. In FSE.
|
| |
202
|
Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ, 189--233.
|
| |
203
|
Sheeran, M., Singh, S., and Stalmarck, G. 2000. Checking safety properties using induction and a SAT-solver. In FMCAD 00: Proceedings of the Symposium on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1954. Springer-Verlag, Berlin, Germany, 108--125.
|
| |
204
|
Shostak, R. 1984. Deciding combinations of theories. J. ACM 31, 1, 1--12.
|
| |
205
|
Silva, J. P. M. and Sakallah, K. A. 1996. Grasp—A new search algorithm for satisfiability. In ICCAD 96: Proceedings of the International Conference on Computer-Aided Design. ACM, New York, 220--227.
|
| |
206
|
Sistla, A., Gyuris, V., and Emerson, E. 2000. SMC: A symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Method. 9, 133--166.
|
| |
207
|
Somenzi, F. 1998. Colorado University decision diagram package. http://vlsi.colorado.edu/pub/.
|
| |
208
|
Stark, E. 1985. A proof technique for rely/guarantee properties. In FSTTCS 1985: Foundations of Software Technology and Theoretical Computer Science, S. N. Maheshwari, Ed. Lecture Notes in Computer Science, vol. 206. Springer-Verlag, Berlin, Germany, 369--391.
|
| |
209
|
Steensgard, B. 1996. Points-to analysis in almost linear time. In POPL 96: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 32--41.
|
| |
210
|
Steffen, B. 1991. Data flow analysis as model checking. In TACS 91: Proceedings of the Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 536. Springer-Verlag, Berlin, Germany, 346--365.
|
| |
211
|
Stern, U. and Dill, D. L. 1998. Using magnetic disk instead of main memory in the murhi verifier. In CAV 98: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 172--183.
|
| |
212
|
Strom, R. and Yemini, S. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12, 1, 157--171.
|
| |
213
|
Sunshine, C. 1978. Survey of protocol definition and verification techniques. Comput. Netw. 2, 346--350.
|
| |
214
|
Sunshine, C., Thompson, D., Erickson, R., Gerhart, S., and Schwabe, D. 1982. Specification and verification of communication protocols in AFFIRM using state transition models. IEEE Trans. Softw. Eng. 8, 5, 460--489.
|
| |
215
|
Suwimonteerabuth, D., Esparza, J., and Schwoon, S. 2008. Symbolic context-bounded analysis of multithreaded Java programs. In SPIN. 270--287.
|
| |
216
|
Tiwari, A. 2004. Termination of linear programs. In CAV 04: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 70--82.
|
| |
217
|
Turing, A. M. 1936. On computable numbers, with an application to the eintscheidungsproblem. In Proceedings of the London Mathematical Soceity. 230--265.
|
| |
218
|
Valmari, A. 1992. A stubborn attack on state explosion. Form. Meth. Syst. Des. 1, 4, 297--322.
|
| |
219
|
Vardi, M. 1991. Verification of concurrent programs—the automata-theoretic framework. Ann. Pure Appl. Logic 51, 79--98.
|
| |
220
|
Vardi, M. 1995. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency—Structure versus Automata (8th Banff Higher Order Workshop Proceedings). Lecture Notes in Computer Science, vol. 1043. Springer-Verlag, Berlin, Germany, 238--266.
|
| |
221
|
Vardi, M. and Wolper, P. 1986. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32, 183--221.
|
| |
222
|
Vardi, M. and Wolper, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1, 1--37.
|
| |
223
|
Velroyen, H. and Rümmer, P. 2008. Non-termination checking for imperative programs. In TAP: Tests and Proofs. Lecture Notes in Computer Science, vol. 4966. Springer-Verlag, Berlin, Germany, 154--170.
|
| |
224
|
Visser, W., Havelund, K., Brat, G., Park, S., and Lerda, F. 2003. Model checking programs. Automat. Softw. Eng. J. 10.
|
| |
225
|
Walukiewicz, I. 1996. Pushdown processes: Games and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 62--74.
|
| |
226
|
Wang, C., Yang, Z., Gupta, A., and Ivancic, F. 2007. Using counterexamples for improving the precision of reachability computation with polyhedra. In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 352--365.
|
| |
227
|
Whaley, J. and Lam, M. S. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI 04: Proceedings of the Symposium on Programming Language Design and Implementation. ACM, New York, 131--144.
|
| |
228
|
Xi, H. and Pfenning, F. 1999. Dependent types in practical programming. In POPL 99: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 214--227.
|
| |
229
|
Xia, S., Vito, B. D., and Muñoz, C. 2005. Automated test generation for engineering applications. In ASE 05: Proceedings of the Symposium on Automated Software Engineering. ACM, New York, 283--286.
|
| |
230
|
Xie, Y. and Aiken, A. A. 2005. Scalable error detection using Boolean satisfiability. In POPL 05: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York.
|
| |
231
|
Yahav, E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic. In POPL 01: Proceedings of the Symposium on Principles of Programming Languages. ACM, New York, 27--40.
|
| |
232
|
Yang, C. H. and Dill, D. L. 1998. Validation with guided search of the state space. In DAC 98: Proceedings of the Symposium on Design Automation Conference. ACM, New York, 599--604.
|
| |
233
|
Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., and O'Hearn, P. W. 2008. Scalable shape analysis for systems code. In CAV 08: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 385--398.
|
| |
234
|
Yang, J., Twohey, P., Engler, D., and Musuvathi, M. 2004. Using model checking to find serious file system errors. In OSDI 04: Proceedings of the Symposium on Operating System Design and Implementation. Usenix Association.
|
| |
235
|
Yang, Z., Wang, C., Gupta, A., and Ivancic, F. 2006. Mixed symbolic representations for model checking software programs. In MEMOCODE. 17--26.
|
| |
236
|
Yannakakis, M. 1990. Graph theoretic methods in database theory. In Proceedings of the 9th ACM Symposium on Principles of Database Systems. ACM, New York, 203--242.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2