מבוא לאימות תוכנה

8.2. מקורות באנגלית

1. "An Analysis of SAT-based Model Checking Techniques in an Industrial Environment", Cadence Design Systems, 2005, Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan and Kenneth L. McMillan
2. "An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking", 2004, Kedar S. Namjoshi
3. "Applying SAT methods in Unbounded Symbolic Model Checking", K. L. McMillan, Cadence Berkeley Labs
4. "Computational tree logic", 2006, Wikipedia.
5. “CTL*”, 2008, Wikipedia.
6. “Davis–Putnam algorithm”, 2009, Wikipedia.
7. “DPLL algorithm”, 2009, Wikipedia.
8. "Graph Algorithms", 1996, Renaud Waldura, http://renaud.waldura.com/portfolio/graph-algorithms/
9. "Model Checking", 1999, MIT Press, Edmund M Clarke, Orna Grumberg and Doron Peled.
10. "Linear temporal logic", 2006, Wikipedia.
11. "Logic in Computer Science(Second Edition)", 2004, Michael Huth and Mark Ryan.
12. "Program Verification", 1992, Addison-Wesley Publishing Company, France Nissim.
13. "Overview of the Temporal Logic CTL*", 2003, Knowledge Representation Lab – Texas Tech University, Edmund M. Clarke, Orna Grumberg, and Doron Peled.
14. "Semantics and Verification of Software - Operational Semantics of WHILE", 2008, RWTH Aachen University, Thomas Noll
15. "Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer", 1981, Irene Greif, Albert R. Meyer
16. "Temporal Logic", 1999, Stanford Encyclopedia of Philosophy (http://plato.stanford.edu/entries/logic-temporal/).
17. "Timed Automata and Timed Computation Tree Logic", 2000, Paul Pettersson.
18. "Tuning SAT checkers for Bounded Model Checking", Ofer Shtrichman
19. "Vacuity Analysis by Fault Simulation", 2008, Luigi Di Guglielmo, Franco Fummi,Graziano Pravadelli