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.
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.
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 http://ceur-ws.org/Vol-1645/paper_4.pdf.
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.
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.
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.
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.
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.
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.
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.
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.
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.
A. Cimatti & A. Griggio (2012):
Software model checking via IC3.
In: CAV,
pp. 277–293,
doi:10.1007/978-3-642-31424-7_23.
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.
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.
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.
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.
C. Flanagan & S. Qadeer (2002):
Predicate abstraction for software verification.
In: POPL,
pp. 191–202,
doi:10.1145/565816.503291.
S. Ghilardi & E. Pagani (2017):
Second Order Quantifier Elimination: towards Verification Applications.
Technical Report.
In preparation.
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.
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.
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.
K. Hoder & N. Bjørner (2012):
Generalized Property Directed Reachability.
In: SAT,
pp. 157–171,
doi:10.1007/978-3-642-31612-8_13.
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.
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.
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.
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.
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.
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.
J. Lambek & P. J. Scott (1988):
Introduction to higher order categorical logic.
Cambridge Studies in Advanced Mathematics 7.
Cambridge University Press,
Cambridge.
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.
T.K. Srikanth & S. Toueg (1987):
Optimal Clock Synchronization.
Journal of the ACM 34(3),
pp. 626–645,
doi:10.1145/28869.28876.
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.
eptcs@eptcs.org