Finding and fixing faults. (English) Zbl 1263.68112
The promises of fault localization and correction for finite state systems sound like magic. However, the algorithm proposed by the authors makes intuitive sense, and it is given a reasonably clear exposition in the paper. The algorithm extracts a “correction” from a winning strategy for a game, constructed from the original program and its specification (expressed in linear temporal logic). The authors apply their algorithm to six examples: unfortunately, all six examples are small in scope and tersely presented. It remains unclear whether larger examples remain tractable with this level of automation.
Reviewer: Johan Georg Granström (Zürich)
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 91A80 | Applications of game theory |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Keywords:
debugging; fault localization; fault correction; verification; games; linear temporal logicReferences:
| [1] | A. Church, Logic, arithmetic and automata, in: Proceedings of the International Mathematical Congress, 1962.; A. Church, Logic, arithmetic and automata, in: Proceedings of the International Mathematical Congress, 1962. · Zbl 0116.33604 |
| [2] | A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proc. Symposium on Principles of Programming Languages (POPL ʼ89), 1989, pp. 179-190.; A. Pnueli, R. Rosner, On the synthesis of a reactive module, in: Proc. Symposium on Principles of Programming Languages (POPL ʼ89), 1989, pp. 179-190. · Zbl 0686.68015 |
| [3] | B. Jobstmann, R. Bloem, Optimizations for LTL synthesis, in: 6th Conference on Formal Methods in Computer Aided Design (FMCADʼ06), 2006, pp. 117-124.; B. Jobstmann, R. Bloem, Optimizations for LTL synthesis, in: 6th Conference on Formal Methods in Computer Aided Design (FMCADʼ06), 2006, pp. 117-124. |
| [4] | B. Jobstmann, S. Galler, M. Weiglhofer, R. Bloem, Anzu: A tool for property synthesis, in: Computer Aided Verification, 2007, pp. 258-262.; B. Jobstmann, S. Galler, M. Weiglhofer, R. Bloem, Anzu: A tool for property synthesis, in: Computer Aided Verification, 2007, pp. 258-262. |
| [5] | Bloem, R.; Galler, S.; Jobstmann, B.; Piterman, N.; Pnueli, A.; Weiglhofer, M., Specify, compile, run: Hardware form PSL, (6th International Workshop on Compiler Optimization Meets Compiler Verification. 6th International Workshop on Compiler Optimization Meets Compiler Verification, Electron. Notes Theor. Comput. Sci. (2007)) |
| [6] | R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, M. Weiglhofer, Automatic hardware synthesis from specifications: A case study, in: Proceedings of the Design, Automation and Test in Europe, 2007, pp. 1188-1193.; R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, M. Weiglhofer, Automatic hardware synthesis from specifications: A case study, in: Proceedings of the Design, Automation and Test in Europe, 2007, pp. 1188-1193. |
| [7] | Jobstmann, B.; Griesmayer, A.; Bloem, R., Program repair as a game, (Etessami, K.; Rajamani, S. K., 17th Conference on Computer Aided Verification (CAVʼ05). 17th Conference on Computer Aided Verification (CAVʼ05), Lecture Notes in Comput. Sci., vol. 3576 (2005), Springer-Verlag), 226-238 · Zbl 1081.68572 |
| [8] | Staber, S.; Jobstmann, B.; Bloem, R., Finding and fixing faults, (Borrione, D.; Paul, W., 13th Conference on Correct Hardware Design and Verification Methods (CHARME ʼ05). 13th Conference on Correct Hardware Design and Verification Methods (CHARME ʼ05), Lecture Notes in Comput. Sci., vol. 3725 (2005), Springer-Verlag), 35-49 · Zbl 1159.68341 |
| [9] | S. Staber, B. Jobstmann, R. Bloem, Diagnosis is repair, in: 16th International Workshop on Principles of Diagnosis, 2005, pp. 169-174.; S. Staber, B. Jobstmann, R. Bloem, Diagnosis is repair, in: 16th International Workshop on Principles of Diagnosis, 2005, pp. 169-174. |
| [10] | E. Clarke, O. Grumberg, K. McMillan, X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, in: Proceedings of the Design Automation Conference, San Francisco, CA, 1995, pp. 427-432.; E. Clarke, O. Grumberg, K. McMillan, X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, in: Proceedings of the Design Automation Conference, San Francisco, CA, 1995, pp. 427-432. |
| [11] | Edelkamp, S.; Lluch-Lafuente, A.; Leue, S., Trail-directed model checking, (Software Model Checking Workshop. Software Model Checking Workshop, Electron. Notes Theor. Comput. Sci., vol. 5 (3) (2001)) · Zbl 1077.68693 |
| [12] | Ravi, K.; Somenzi, F., Minimal assignments for bounded model checking, (International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACASʼ04). International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACASʼ04), Barcelona, Spain, 2004. International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACASʼ04). International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACASʼ04), Barcelona, Spain, 2004, Lecture Notes in Comput. Sci., vol. 2988 (2004)), 31-45 · Zbl 1126.68486 |
| [13] | Zeller, A.; Hildebrandt, R., Simplifying and isolating failure-inducing input, IEEE Trans. Software Engrg., 28, 2, 183-200 (2002) |
| [14] | Jin, H.; Ravi, K.; Somenzi, F., Fate and free will in error traces, Software Tools Technol. Transfer, 6, 2, 102-116 (2004) |
| [15] | A. Zeller, Isolating cause-effect chains from computer programs, in: 10th International Symposium on the Foundations of Software Engineering (FSE-10), 2002, pp. 1-10.; A. Zeller, Isolating cause-effect chains from computer programs, in: 10th International Symposium on the Foundations of Software Engineering (FSE-10), 2002, pp. 1-10. |
| [16] | Groce, A.; Visser, W., What went wrong: Explaining counterexamples, (Model Checking of Software: 10th International SPIN Workshop. Model Checking of Software: 10th International SPIN Workshop, Lecture Notes in Comput. Sci., vol. 2648 (2003), Springer-Verlag), 121-135 · Zbl 1023.68531 |
| [17] | T. Ball, M. Naik, S.K. Rajamani, From symptom to cause: Localizing errors in counterexample traces, in: 30th Symposium on Principles of Programming Languages (POPL 2003), 2003, pp. 97-105.; T. Ball, M. Naik, S.K. Rajamani, From symptom to cause: Localizing errors in counterexample traces, in: 30th Symposium on Principles of Programming Languages (POPL 2003), 2003, pp. 97-105. |
| [18] | M. Renieris, S.P. Reiss, Fault localization with nearest neighbor queries, in: International Conference on Automated Software Engineering, Montreal, Canada, 2003, pp. 30-39.; M. Renieris, S.P. Reiss, Fault localization with nearest neighbor queries, in: International Conference on Automated Software Engineering, Montreal, Canada, 2003, pp. 30-39. |
| [19] | Groce, A.; Chaki, S.; Kroening, D.; Strichman, O., Error explanation with distance metrics, Software Tools Technol. Transfer, 8, 229-247 (2006) |
| [20] | J.C. Madre, O. Coudert, J.P. Billon, Automating the diagnosis and the rectification of design error with PRIAM, in: Proceedings of the International Conference on Computer-Aided Design, 1989, pp. 30-33.; J.C. Madre, O. Coudert, J.P. Billon, Automating the diagnosis and the rectification of design error with PRIAM, in: Proceedings of the International Conference on Computer-Aided Design, 1989, pp. 30-33. |
| [21] | H.-T. Liaw, J.-H. Tsiah, C.-S. Lin, Efficient automatic diagnosis of digital circuits, in: Proceedings of the International Conference on Computer-Aided Design, 1990, pp. 464-467.; H.-T. Liaw, J.-H. Tsiah, C.-S. Lin, Efficient automatic diagnosis of digital circuits, in: Proceedings of the International Conference on Computer-Aided Design, 1990, pp. 464-467. |
| [22] | Chung, P.-Y.; Wang, Y.-M.; Hajj, I. N., Logic design error diagnosis and correction, IEEE Trans. Very Large Scale Integration (VLSI) Systems, 2, 320-332 (1994) |
| [23] | M. Tomita, T. Yamamoto, F. Sumikawa, K. Hirano, Rectification of multiple logic design errors in multiple output circuits, in: Proceedings of the Design Automation Conference, 1994, pp. 212-217,.; M. Tomita, T. Yamamoto, F. Sumikawa, K. Hirano, Rectification of multiple logic design errors in multiple output circuits, in: Proceedings of the Design Automation Conference, 1994, pp. 212-217,. |
| [24] | Wahba, A.; Borrione, D., Design error diagnosis in sequential circuits, (Correct Hardware Design and Verification Methods (CHARMEʼ95). Correct Hardware Design and Verification Methods (CHARMEʼ95), Lecture Notes in Comput. Sci., vol. 987 (1995)), 171-188 |
| [25] | Buccafurri, F.; Eiter, T.; Gottlob, G.; Leone, N., Enhancing model checking in verification by AI techniques, Artificial Intelligence, 112, 57-104 (1999) · Zbl 0996.68104 |
| [26] | A. Ebnenasir, S. Kulkarni, B. Bonakdarpour, Revising UNITY programs: Possibilities and limitations, in: Proc. Principles of Distributed Systems (OPODISʼ05), 2005, pp. 275-290.; A. Ebnenasir, S. Kulkarni, B. Bonakdarpour, Revising UNITY programs: Possibilities and limitations, in: Proc. Principles of Distributed Systems (OPODISʼ05), 2005, pp. 275-290. |
| [27] | K.-H. Chang, I.L. Markov, V. Bertacco, Fixing design error with counterexamples and resynthesis, in: Asia and South Pacific Design Automation Conference (ASP-DACʼ07), 2007, pp. 944-949.; K.-H. Chang, I.L. Markov, V. Bertacco, Fixing design error with counterexamples and resynthesis, in: Asia and South Pacific Design Automation Conference (ASP-DACʼ07), 2007, pp. 944-949. |
| [28] | M.U. Janjua, A. Mycroft, Automatic correction to safety violations in programs, in: Thread Verification (TVʼ06), 2006, unpublished.; M.U. Janjua, A. Mycroft, Automatic correction to safety violations in programs, in: Thread Verification (TVʼ06), 2006, unpublished. |
| [29] | A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, S.A. Seshia, Combinatorial sketching for finite programs, in: Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOSʼ06), 2006, pp. 404-415.; A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, S.A. Seshia, Combinatorial sketching for finite programs, in: Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOSʼ06), 2006, pp. 404-415. |
| [30] | Console, L.; Friedrich, G.; Theseider Dupré, D., Model-based diagnosis meets error diagnosis in logic programs, (Proceedings of the International Joint Conference on Artificial Intelligence (IJCAIʼ93) (1993), Morgan Kaufmann), 1494-1499 |
| [31] | M. Stumptner, F. Wotawa, A model-based approach to software debugging, in: Proceedings on the Seventh International Workshop on Principles of Diagnosis, 1996.; M. Stumptner, F. Wotawa, A model-based approach to software debugging, in: Proceedings on the Seventh International Workshop on Principles of Diagnosis, 1996. |
| [32] | G. Friedrich, M. Stumptner, F. Wotawa, Model-based diagnosis of hardware designs, in: European Conference on Artificial Intelligence, 1996, pp. 491-495.; G. Friedrich, M. Stumptner, F. Wotawa, Model-based diagnosis of hardware designs, in: European Conference on Artificial Intelligence, 1996, pp. 491-495. · Zbl 0996.68210 |
| [33] | C. Mateis, M. Stumptner, F. Wotawa, A value-based diagnosis model for Java programs, in: Proceedings of the Eleventh International Workshop on Principles of Diagnosis, 2000.; C. Mateis, M. Stumptner, F. Wotawa, A value-based diagnosis model for Java programs, in: Proceedings of the Eleventh International Workshop on Principles of Diagnosis, 2000. |
| [34] | Console, L.; Torasso, P., A spectrum of logical definitions of model-based diagnosis, Comput. Intell., 7, 3, 133-141 (1991) |
| [35] | Poole, D. L.; Goebel, R.; Aleliunas, R., Theorist: a logical reasoning system for defaults and diagnosis, (Cercone, N.; McCalla, G., The Knowledge Frontier: Essays in the Representation of Knowledge (1987), Springer-Verlag), 331-352 |
| [36] | de Kleer, J.; Williams, B. C., Diagnosing multiple faults, Artificial Intelligence, 32, 97-130 (1987) · Zbl 0642.94045 |
| [37] | Reiter, R., A theory of diagnosis from first principles, Artificial Intelligence, 32, 57-95 (1987) · Zbl 0643.68122 |
| [38] | S. Staber, G. Fey, R. Bloem, R. Drechsler, Automatic fault localization for property checking, in: Second International Haifa Verification Conference (HVC 2006), 2006, pp. 50-64.; S. Staber, G. Fey, R. Bloem, R. Drechsler, Automatic fault localization for property checking, in: Second International Haifa Verification Conference (HVC 2006), 2006, pp. 50-64. |
| [39] | Peischl, B.; Wotawa, F., Automated source-level error localization in hardware designs, IEEE Design Test Comput., 23, 8-19 (2006) |
| [40] | M. Fahim Ali, A. Veneris, S. Safarpur, R. Drechsler, A. Smith, M. Abadir, Debugging sequential circuits using Boolean satisfiability, in: International Conference on Computer Aided Design, 2004, pp. 204-209.; M. Fahim Ali, A. Veneris, S. Safarpur, R. Drechsler, A. Smith, M. Abadir, Debugging sequential circuits using Boolean satisfiability, in: International Conference on Computer Aided Design, 2004, pp. 204-209. |
| [41] | M. Stumptner, F. Wotawa, Debugging functional programs, in: Proceedings on the 16th International Joint Conference on Artificial Intelligence, 1999.; M. Stumptner, F. Wotawa, Debugging functional programs, in: Proceedings on the 16th International Joint Conference on Artificial Intelligence, 1999. · Zbl 1045.68961 |
| [42] | W. Hamscher, R. Davis, Diagnosing circuits with state: An inherently underconstrained problem, in: Proceedings of the Fourth National Conference on Artificial Intelligence (AAAIʼ84), 1984, pp. 142-147.; W. Hamscher, R. Davis, Diagnosing circuits with state: An inherently underconstrained problem, in: Proceedings of the Fourth National Conference on Artificial Intelligence (AAAIʼ84), 1984, pp. 142-147. |
| [43] | A. Pnueli, The temporal logic of programs, in: IEEE Symposium on Foundations of Computer Science, Providence, RI, 1977, pp. 46-57.; A. Pnueli, The temporal logic of programs, in: IEEE Symposium on Foundations of Computer Science, Providence, RI, 1977, pp. 46-57. |
| [44] | Clarke, E. M.; Grumberg, O.; Peled, D. A., Model Checking (1999), MIT Press: MIT Press Cambridge, MA |
| [45] | Ramadge, P. J.G.; Wonham, W. M., The control of discrete event systems, Proc. IEEE, 77, 81-98 (1989) |
| [46] | P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, 1983, pp. 185-194.; P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, 1983, pp. 185-194. |
| [47] | O. Lichtenstein, A. Pnueli, Checking that finite state concurrent programs satisfy their linear specification, in: Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, 1985, pp. 97-107.; O. Lichtenstein, A. Pnueli, Checking that finite state concurrent programs satisfy their linear specification, in: Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, 1985, pp. 97-107. |
| [48] | Thomas, W., On the synthesis of strategies in infinite games, (Proc. 12th Annual Symposium on Theoretical Aspects of Computer Science. Proc. 12th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Comput. Sci., vol. 900 (1995), Springer-Verlag), 1-13 · Zbl 1379.68233 |
| [49] | O. Kupferman, M.Y. Vardi, Freedom, weakness, and determinism: From linear-time to branching-time, in: Proc. 13th IEEE Symposium on Logic in Computer Science, 1998.; O. Kupferman, M.Y. Vardi, Freedom, weakness, and determinism: From linear-time to branching-time, in: Proc. 13th IEEE Symposium on Logic in Computer Science, 1998. · Zbl 0945.68522 |
| [50] | Sebastiani, R.; Tonetta, S., More deterministic vs. “smaller” Büchi automata for efficient LTL model checking, (Correct Hardware Design and Verification Methods (CHARMEʼ03). Correct Hardware Design and Verification Methods (CHARMEʼ03), Lecture Notes in Comput. Sci., vol. 2860 (2003), Springer-Verlag: Springer-Verlag Berlin), 126-140 · Zbl 1179.68095 |
| [51] | M. Maidl, The common fragment of CTL and LTL, in: Proc. 41th Annual Symposium on Foundations of Computer Science, 2000, pp. 643-652.; M. Maidl, The common fragment of CTL and LTL, in: Proc. 41th Annual Symposium on Foundations of Computer Science, 2000, pp. 643-652. |
| [52] | Gerth, R.; Peled, D.; Vardi, M. Y.; Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, (Protocol Specification, Testing, and Verification (1995), Chapman & Hall), 3-18 |
| [53] | Somenzi, F.; Bloem, R., Efficient Büchi automata from LTL formulae, (Emerson, E. A.; Sistla, A. P., Twelfth Conference on Computer Aided Verification (CAVʼ00). Twelfth Conference on Computer Aided Verification (CAVʼ00), Lecture Notes in Comput. Sci., vol. 1855 (2000), Springer-Verlag: Springer-Verlag Berlin), 248-263 · Zbl 0974.68086 |
| [54] | R. Alur, S. La Torre, Deterministic generators and games for LTL fragments, in: Symposium on Logic in Computer Science (LICSʼ01), 2001, pp. 291-302.; R. Alur, S. La Torre, Deterministic generators and games for LTL fragments, in: Symposium on Logic in Computer Science (LICSʼ01), 2001, pp. 291-302. · Zbl 1366.03181 |
| [55] | Fortune, S.; Hopcroft, J.; Wyllie, J., The directed subgraph homeomorphism problem, Theoret. Comput. Sci., 10, 111-121 (1980) · Zbl 0419.05028 |
| [56] | Lin, F.; Wonham, W. M., On observability of discrete-event systems, Inform. Sci., 44, 173-198 (1988) · Zbl 0644.93008 |
| [57] | Vardi, M. Y., An automata-theoretic approach to fair realizability and synthesis, (Seventh Conference on Computer Aided Verification (CAVʼ95) (1995), Springer-Verlag), 267-278 |
| [58] | Kupferman, O.; Vardi, M. Y., Churchʼs problem revisited, Bull. Symbolic Logic, 5, 245-263 (1999) · Zbl 0932.03029 |
| [59] | Hachtel, G. D.; Somenzi, F., Logic Synthesis and Verification Algorithms (1996), Kluwer Academic Publishers: Kluwer Academic Publishers Boston, MA · Zbl 0861.94035 |
| [60] | E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: Proceedings of the First Annual Symposium of Logic in Computer Science, 1986, pp. 267-278.; E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: Proceedings of the First Annual Symposium of Logic in Computer Science, 1986, pp. 267-278. |
| [61] | Ravi, K.; Bloem, R.; Somenzi, F., A comparative study of symbolic algorithms for the computation of fair cycles, (Hunt, W. A.; Johnson, S. D., Formal Methods in Computer Aided Design. Formal Methods in Computer Aided Design, Lecture Notes in Comput. Sci., vol. 1954 (2000), Springer-Verlag), 143-160 |
| [62] | Bloem, R.; Gabow, H. N.; Somenzi, F., An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps, Formal Methods Syst. Design, 28, 1, 37-56 (2006) · Zbl 1110.68161 |
| [63] | Brayton, R. K., VIS: A system for verification and synthesis, (Henzinger, T.; Alur, R., Eighth Conference on Computer Aided Verification (CAVʼ96). Eighth Conference on Computer Aided Verification (CAVʼ96), Lecture Notes in Comput. Sci., vol. 1102 (1996), Springer-Verlag: Springer-Verlag Rutgers University), 428-432 · Zbl 1102.68301 |
| [64] | Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, (Proceedings of the 29th Symposium on Principles of Programming Languages (POPLʼ02) (2002), ACM Press), 58-70 · Zbl 1323.68374 |
| [65] | Peterson, G. L., Myths about the mutual exclusion problem, Inform. Process. Lett., 12, 115-116 (1981) · Zbl 0474.68031 |
| [66] | Griesmayer, A.; Staber, S.; Bloem, R., Automated fault localization for C programs, (Workshop on Verification and Debugging (V&Dʼ06). Workshop on Verification and Debugging (V&Dʼ06), Electron. Notes Theor. Comput. Sci., vol. 174 (2006)), 95-111 |
| [67] | Do, H.; Elbaum, S. G.; Rothermel, G., Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact, Empirical Software Engrg., 10, 405-435 (2005) |
| [68] | E.M. Clarke, D. Kroening, F. Lerda, A tool for checking ANSI-C programs, in: Tools and Algorithms for the Construction and Analysis of Systems (TACASʼ04), 2004, pp. 168-176.; E.M. Clarke, D. Kroening, F. Lerda, A tool for checking ANSI-C programs, in: Tools and Algorithms for the Construction and Analysis of Systems (TACASʼ04), 2004, pp. 168-176. · Zbl 1126.68470 |
| [69] | P. Anderson, T. Teitelbaum, Software inspection using CodeSurfer, in: Workshop on Inspection in Software Engineering, 2001.; P. Anderson, T. Teitelbaum, Software inspection using CodeSurfer, in: Workshop on Inspection in Software Engineering, 2001. |
| [70] | Vis verification benchmarks, http://vlsi.colorado.edu/ vis; Vis verification benchmarks, http://vlsi.colorado.edu/ vis |
| [71] | A.J. Hu, D. Dill, Reducing BDD size by exploiting functional dependencies, in: Proceedings of the Design Automation Conference, Dallas, TX, 1993, pp. 266-271.; A.J. Hu, D. Dill, Reducing BDD size by exploiting functional dependencies, in: Proceedings of the Design Automation Conference, Dallas, TX, 1993, pp. 266-271. |
| [72] | Ernst, M. D.; Cockrell, J.; Griswold, W. G.; Notkin, D., Dynamically discovering likely program invariants to support program evolution, IEEE Trans. Software Engrg., 27, 2, 1-25 (2001) |
| [73] | S. Staber, R. Bloem, Fault localization and correction with QBF, in: Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), 2007, pp. 355-368.; S. Staber, R. Bloem, Fault localization and correction with QBF, in: Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), 2007, pp. 355-368. · Zbl 1214.94086 |
| [74] | Ball, T.; Rajamani, S. K., Automatically validating temporal safety properties of interfaces, (Dwyer, M., 8th International SPIN Workshop. 8th International SPIN Workshop, Lecture Notes in Comput. Sci., vol. 2057 (2001), Springer-Verlag: Springer-Verlag Toronto), 103-122 · Zbl 0985.68641 |
| [75] | Griesmayer, A.; Bloem, R.; Cook, B., Repair of Boolean programs with an application to C, (18th Conference on Computer Aided Verification (CAVʼ06). 18th Conference on Computer Aided Verification (CAVʼ06), Lecture Notes in Comput. Sci., vol. 4144 (2006)), 358-371 · Zbl 1188.68188 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
