1. Rajeev Alur & Thomas A. Henzinger (1991): Logics and Models of Real Time: A Survey. In: REX Workshop, pp. 74–106, doi:10.1007/BFb0031988.
  2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke & Yunshan Zhu (1999): Symbolic Model Checking without BDDs. In: TACAS, pp. 193–207, doi:10.1007/3-540-49059-0_14.
  3. Armin Biere, Edmund M. Clarke & Yunshan Zhu: Multiple State and Single State Tableaux for Combining Local and Global Model Checking, doi:10.1007/3-540-48092-7_8.
  4. Jan Broersen, Frank Dignum, Virginia Dignum & John-Jules Ch. Meyer (2004): Designing a Deontic Logic of Deadlines. In: DEON, doi:10.1007/978-3-540-25927-5_5.
  5. Jerry R. Burch & all. (1992): Symbolic Model Checking: 10^20 States and Beyond. Inf. Comput. 98(2), pp. 142–170, doi:10.1016/0890-5401(92)90017-A.
  6. A. Cimatti, M. Roveri, V. Schuppan & S. Tonetta (2007): Boolean Abstraction for Temporal Logic Satisfiability. In: CAV, pp. 532–546, doi:10.1007/978-3-540-73368-3_53.
  7. Elio Damaggio, Alin Deutsch & Victor Vianu (2011): Artifact systems with data dependencies and arithmetic. In: ICDT, pp. 66–77, doi:10.1145/1938551.1938563.
  8. Martin Davis, George Logemann & Donald W. Loveland (1962): A machine program for theorem-proving. Commun. ACM 5(7), pp. 394–397, doi:10.1145/368273.368557.
  9. E. Emerson (1990): Temporal and Modal Logic. HTCS, Volume B: Formal Models and Sematics (B).
  10. Stephen Fenech, Gordon J. Pace & Gerardo Schneider (2009): Automatic Conflict Detection on Contracts. In: ICTAC, pp. 200–214, doi:10.1007/978-3-642-03466-4_13.
  11. Michael J. Fischer & Richard E. Ladner (1979): Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci. 18(2), pp. 194–211, doi:10.1016/0022-0000(79)90046-1.
  12. Michael Fisher (1991): A Resolution Method for Temporal Logic. In: IJCAI, pp. 99–104.
  13. Malay K. Ganai, Aarti Gupta & Pranav Ashar (2005): Beyond safety: customized SAT-based model checking. In: DAC, pp. 738–743, doi:10.1145/1065579.1065773.
  14. Rob Gerth, Doron Peled, Moshe Y. Vardi & Pierre Wolper (1995): Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp. 3–18.
  15. Aditya Ghose & George Koliadis (2007): Auditing Business Process Compliance. In: ICSOC, pp. 169–180, doi:10.1007/978-3-540-74974-5_14.
  16. C. Giblin, A. Liu, S. Müller & B. Pfitzmann (2005): Regulations Expressed As Logical Models (REALM). In: JURIX, pp. 37–48.
  17. Keijo Heljanko, Tommi A. Junttila & Timo Latvala (2005): Incremental and Complete Bounded Model Checking for Full PLTL. In: CAV, pp. 98–111, doi:10.1007/11513988_10.
  18. Toni Jussila & Armin Biere (2007): Compressing BMC Encodings with QBF. Electr. Notes Theor. Comput. Sci. 174(3), pp. 45–56, doi:10.1016/j.entcs.2006.12.022.
  19. Y. Kesten, Z. Manna, H. McGuire & A. Pnueli (1993): A Decision Algorithm for Full Propositional Temporal Logic. In: CAV, pp. 97–109, doi:10.1007/3-540-56922-7_9.
  20. Annapaola Marconi & Marco Pistore (2009): Synthesis and Composition of Web Services. In: SFM, pp. 89–157, doi:10.1007/978-3-642-01918-0_3.
  21. M. Montali, M. Pesic, W. v.d. Aalst, F. Chesani & P. Mello (2010): Declarative specification and verification of service choreographies. TWEB 4(1), doi:10.1145/1658373.1658376.
  22. M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang & S. Malik (2001): Chaff: Engineering an Efficient SAT Solver. In: DAC, pp. 530–535. Available at
  23. Viktor Schuppan (2010): Towards a notion of unsatisfiable and unrealizable cores for LTL. Science of Computer Programming, doi:10.1016/j.scico.2010.11.004.
  24. Mary Sheeran, Satnam Singh & Gunnar Stålmarck (2000): Checking Safety Properties Using Induction and a SAT-Solver. In: FMCAD, pp. 108–125, doi:10.1007/3-540-40922-X_8.
  25. Robert Endre Tarjan (1972): Depth-First Search and Linear Graph Algorithms. SIAM J. Comput. 1(2), pp. 146–160, doi:10.1137/0201010.
  26. K. Xu, Y. Liu & C. Wu (2008): BPSL Modeler - Visual Notation Language for Intuitive Business Property Reasoning. ENTCS 211, doi:10.1016/j.entcs.2008.04.043.
  27. L. Zhang, C. Madigan, M. Moskewicz & S. Malik (2001): Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: ICCAD, pp. 279–285. Available at
  28. L. Zhang & S. Malik (2003): Extracting small unsatisfiable cores from unsatisfiable Boolean formula.. In: In Prelim. Proc. Sixth Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT\IeC 03).

Comments and questions to:
For website issues: