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.
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.
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.
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.
Edsger W. Dijkstra (1974):
Self-stabilizing Systems in Spite of Distributed Control.
Commun. ACM 17(11),
pp. 643–644,
doi:10.1145/361179.361202.
Bernd Finkbeiner & Sven Schewe (2013):
Bounded synthesis.
STTT 15(5-6),
pp. 519–539,
doi:10.1007/s10009-012-0228-z.
Adrià Gascón & Ashish Tiwari:
Sal modules of the running example.
Available at: http://www.csl.sri.com/users/tiwari/softwares/synth_distributed.
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.
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.
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.
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.
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.
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.
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.
Nancy A. Lynch (1996):
Distributed Algorithms.
Morgan Kaufmann.
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.
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.
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.
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.
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.
(2003):
The SAL intermediate language.
Computer Science Laboratory, SRI International, Menlo Park, CA. http://sal.csl.sri.com/.
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.
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.
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.
Saurabh Srivastava, Sumit Gulwani & Jeffrey S. Foster (2010):
From program verification to program synthesis.
In: POPL,
pp. 313–326,
doi:10.1145/1706299.1706337.
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.
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.