1. P. A. Abdulla, K. Cerans, B. Jonsson & Y.-K. Tsay (1996): General Decidability Theorems for Infinite-State Systems. In: Proc. of LICS, pp. 313–321, doi:10.1109/LICS.1996.561359.
  2. P. A. Abdulla, G. Delzanno, N. B. Henda & A. Rezine (2007): Regular Model Checking Without Transducers. In: TACAS, LNCS 4424, pp. 721–736, doi:10.1007/978-3-540-71209-1_56.
  3. F. Alberti, S. Ghilardi, A. Orsini & E. Pagani (2016): Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies. In: Proc. CILC, CEUR Proceedings, pp. 102–117. Available at
  4. F. Alberti, S. Ghilardi & E. Pagani (2016): Counting Constraints in Flat Array Fragments. In: Proc. IJCAR, Lecture Notes in Computer Science 9706, pp. 65–81, doi:10.1007/978-3-319-40229-1_6.
  5. F. Alberti, S. Ghilardi & E. Pagani (2017): Cardinality Constraints for Arrays (decidability results and applications). Formal Methods in System Design, doi:10.1007/s10703-017-0279-6. To appear.
  6. F. Alberti, S. Ghilardi & N. Sharygina (2015): Decision Procedures for Flat Array Properties. Journal of Automated Reasoning 54(4), pp. 327–352, doi:10.1007/s10817-015-9323-7.
  7. Peter B. Andrews (2002): An introduction to mathematical logic and type theory: to truth through proof, 2nd edition, Applied Logic Series 27. Kluwer Academic Publishers, Dordrecht, doi:10.1007/978-94-015-9934-4.
  8. M. Biely, B. Charron-Bost, A. Gaillard, M. Hutle, A. Schiper & J. Widder (2007): Tolerating corrupted communication. In: Proc. PODC, pp. 244–253, doi:10.1145/1281100.1281136.
  9. N. Bjørner, K. von Gleissenthall & A. Rybalchenko (2016): Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. In: Proc. of PLDI, doi:10.1145/2980983.2908129.
  10. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri & S. Tonetta (2014): The nuXmv Symbolic Model Checker. In: CAV, pp. 334–342, doi:10.1007/978-3-319-08867-9_22.
  11. B. Charron-Bost, H. Debrat & S. Merz (2011): Formal Verification of Consensus Algorithms Tolerating Malicious Faults. In: Stabilization, Safety, and Security of Distributed Systems. Springer LNCS, pp. 120–134, doi:10.1007/978-3-642-24550-3_11.
  12. B. Charron-Bost & A. Schiper (2009): The heard-of model: computing in distributed systems with benign faults. Distributed Computing, pp. 49–71, doi:10.1007/s00446-009-0084-6.
  13. A. Cimatti & A. Griggio (2012): Software model checking via IC3. In: CAV, pp. 277–293, doi:10.1007/978-3-642-31424-7_23.
  14. G. Delzanno (2003): Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design 23(3), pp. 257–301, doi:10.1023/A:1026276129010.
  15. G. Delzanno, J. Esparza & A. Podelski (1999): Constraint-Based Analysis of Broadcast Protocols. In: Proc. of CSL, LNCS 1683, pp. 50–66, doi:10.1007/3-540-48168-0_5.
  16. C. Dragoj, T. Henzinger, H. Veith, J. Widder & D. Zufferey (2014): A Logic-based Framework for Verifying Consensus Algorithms. In: Proc. of VMCAI, doi:10.1007/978-3-642-54013-4_10.
  17. J. Esparza, A. Finkel & R. Mayr (1999): On the Verification of Broadcast Protocols. In: Proc. of LICS. IEEE Computer Society, pp. 352–359, doi:10.1109/LICS.1999.782630.
  18. C. Flanagan & S. Qadeer (2002): Predicate abstraction for software verification. In: POPL, pp. 191–202, doi:10.1145/565816.503291.
  19. S. Ghilardi & E. Pagani (2017): Second Order Quantifier Elimination: towards Verification Applications. Technical Report. In preparation.
  20. S. Ghilardi & S. Ranise (2010): Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. Logical Methods in Computer Science 6(4), doi:10.2168/LMCS-6(4:10)2010.
  21. S. Ghilardi & S. Ranise (2010): MCMT: A Model Checker Modulo Theories. In: IJCAR, pp. 22–29, doi:10.1007/978-3-642-14203-1_3.
  22. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli & Jorge A. Navas (2015): The SeaHorn Verification Framework. In: CAV, pp. 343–361, doi:10.1007/978-3-319-21690-4_20.
  23. K. Hoder & N. Bjørner (2012): Generalized Property Directed Reachability. In: SAT, pp. 157–171, doi:10.1007/978-3-642-31612-8_13.
  24. K. Hoder, N. Bjørner & L. deMoura (2011): μZ– An Efficient Engine for Fixed Points with Constraints. In: CAV, pp. 457–462, doi:10.1007/978-3-642-22110-1_36.
  25. A. John, I. Konnov, U. Schmid, H. Veith & J. Widder (2013): Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proc. FMCAD, pp. 201–209, doi:10.1109/FMCAD.2013.6679411.
  26. A. John, I. Konnov, U. Schmid, H. Veith & J. Widder (2013): Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. In: Proc. SPIN 7976, pp. 209–226, doi:10.1007/978-3-642-39176-7_14.
  27. I. Konnov, H. Veith & J. Widder (2015): What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In: PSI, pp. 6–21, doi:10.1007/978-3-319-41579-6_2.
  28. I.. Konnov, H. Veith & J. Widder (2017): On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Inf. Comput. 252, pp. 95–109, doi:10.1007/978-3-662-44584-6_10.
  29. Viktor Kuncak, Huu Hai Nguyen & Martin Rinard (2006): Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning 36(3), doi:10.1007/s10817-006-9042-1.
  30. J. Lambek & P. J. Scott (1988): Introduction to higher order categorical logic. Cambridge Studies in Advanced Mathematics 7. Cambridge University Press, Cambridge.
  31. Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli & Clark W. Barrett (2015): Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In: Proc. CAV, pp. 198–216, doi:10.1007/978-3-319-21668-3_12.
  32. T.K. Srikanth & S. Toueg (1987): Optimal Clock Synchronization. Journal of the ACM 34(3), pp. 626–645, doi:10.1145/28869.28876.
  33. T.K. Srikanth & S. Toueg (1987): Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing 2(2), pp. 80–94, doi:10.1007/BF01667080.

Comments and questions to:
For website issues: