References

  1. Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-guided synthesis. In: FMCAD, pp. 1–17, doi:10.1109/FMCAD.2013.6679385.
  2. A. Biere, F. Lonsing & M. Seidl (2011): Blocked Clause Elimination for QBF. In: CADE, pp. 101–115, doi:10.1007/978-3-642-22438-6_10.
  3. Roderick Bloem, Robert Könighofer & Martina Seidl (2014): SAT-Based Synthesis Methods for Safety Specs. In: VMCAI, pp. 1–20, doi:10.1007/978-3-642-54013-4_1.
  4. Chih-Hong Cheng, Natarajan Shankar, Harald Ruess & Saddek Bensalem (2013): EFSMT: A Logical Framework for Cyber-Physical Systems. CoRR abs/1306.3456. Available at http://arxiv.org/abs/1306.3456.
  5. Edsger W. Dijkstra (1974): Self-stabilizing Systems in Spite of Distributed Control. Commun. ACM 17(11), pp. 643–644, doi:10.1145/361179.361202.
  6. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. STTT 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  7. Adrià Gascón & Ashish Tiwari: Sal modules of the running example. Available at: http://www.csl.sri.com/users/tiwari/softwares/synth_distributed.
  8. Adria Gascón & Ashish Tiwari (2014): A Synthesized Algorithm for Interactive Consistency. In: NASA Formal Methods, pp. 270–284, doi:10.1007/978-3-319-06200-6_23.
  9. M. Janota, W. Klieber, J. Marques-Silva & E. M. Clarke (2012): Solving QBF with Counterexample Guided Refinement. In: SAT, pp. 114–128, doi:10.1007/978-3-642-31612-8_10.
  10. Mikolás Janota, Radu Grigore & Joao Marques-Silva (2013): On QBF Proofs and Preprocessing. In: LPAR, pp. 473–489. Available at 10.1007/978-3-642-45221-5_32.
  11. Mikolás Janota, William Klieber, João Marques-Silva & Edmund M. Clarke (2012): Solving QBF with Counterexample Guided Refinement. In: SAT, pp. 114–128, doi:10.1007/978-3-642-31612-8_10.
  12. Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith & Josef Widder (2013): Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201–209, doi:10.1109/FMCAD.2013.6679411.
  13. Leslie Lamport, Robert E. Shostak & Marshall C. Pease (1982): The Byzantine Generals Problem. ACM Trans. Program. Lang. Syst. 4(3), pp. 382–401, doi:10.1145/357172.357176.
  14. Patrick Lincoln & John M. Rushby (1993): The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. In: CAV, pp. 292–304, doi:10.1007/3-540-56922-7_24.
  15. Florian Lonsing & Armin Biere (2010): DepQBF: A Dependency-Aware QBF Solver. JSAT 7(2-3), pp. 71–76. Available at http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_6_Lonsing.pdf.
  16. Nancy A. Lynch (1996): Distributed Algorithms. Morgan Kaufmann.
  17. Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea & Ashish Tiwari (2004): SAL 2. In: CAV, pp. 496–500, doi:10.1007/978-3-540-27813-9_45.
  18. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl & Armin Biere (2012): Resolution-Based Certificate Extraction for QBF - (Tool Presentation). In: SAT, pp. 430–435, doi:10.1007/978-3-642-31612-8_33.
  19. Oswaldo Olivo & E. Allen Emerson (2011): A More Efficient BDD-Based QBF Solver. In: CP, pp. 675–690, doi:10.1007/978-3-642-23786-7_51.
  20. Sam Owre, John M. Rushby, Natarajan Shankar & Friedrich W. von Henke (1993): Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. In: FME, pp. 482–500, doi:10.1007/BFb0024663.
  21. Darsh P. Ranjan, Daijue Tang & Sharad Malik (2004): A Comparative Study of 2QBF Algorithms. In: SAT. Available at http://www.satisfiability.org/SAT04/programme/113.pdf.
  22. John M. Rushby & Friedrich W. von Henke (1993): Formal Verification of Algorithms for Critical Systems. IEEE Trans. Software Eng. 19(1), pp. 13–23, doi:10.1109/32.210304.
  23. (2003): The SAL intermediate language. Computer Science Laboratory, SRI International, Menlo Park, CA. http://sal.csl.sri.com/.
  24. Natarajan Shankar (1992): Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization. In: FTRTFT, pp. 217–236, doi:10.1007/3-540-55092-5_12.
  25. Armando Solar-Lezama, Rodric M. Rabbah, Rastislav Bodík & Kemal Ebcioglu (2005): Programming by sketching for bit-streaming programs. In: PLDI, pp. 281–294, doi:10.1145/1065010.1065045.
  26. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia & Vijay A. Saraswat (2006): Combinatorial Sketching for Finite Programs. In: ASPLOS, pp. 404–415, doi:10.1145/1168857.1168907.
  27. Saurabh Srivastava, Sumit Gulwani & Jeffrey S. Foster (2010): From program verification to program synthesis. In: POPL, pp. 313–326, doi:10.1145/1706299.1706337.
  28. Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M. K. Martin & Rajeev Alur (2013): TRANSIT: specifying protocols with concolic snippets. In: PLDI, pp. 287–296, doi:10.1145/2462156.2462174.
  29. Yinlei Yu & Sharad Malik (2005): Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice. In: ASP-DAC, pp. 1047–1051, doi:10.1145/1120725.1120821.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org