Ausgabe 3/2017
Special issue on Recent topics in SMT
Inhalt (8 Artikel)
Open Access
New techniques for linear arithmetic: cubes and equalities
Martin Bromberger, Christoph Weidenbach
Solving quantified linear arithmetic by counterexample-guided instantiation
Andrew Reynolds, Tim King, Viktor Kuncak
Open Access
NP-completeness of small conflict set generation for congruence closure
Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
Cardinality constraints for arrays (decidability results and applications)
F. Alberti, S. Ghilardi, E. Pagani
Compositional entailment checking for a fragment of separation logic
Constantin Enea, Ondřej Lengál, Mihaela Sighireanu, Tomáš Vojnar
Open Access
Propagation based local search for bit-precise reasoning
Aina Niemetz, Mathias Preiner, Armin Biere