R. Bagnara, P. M. Hill & E. Zaffanella (2008):
The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems.
Science of Computer Programming 72(1–2),
pp. 3–21.
Available at http://dx.doi.org/10.1016/j.scico.2007.08.001.
T. Ball, V. Levin & S. K. Rajamani (2011):
A decade of software model checking with SLAM.
Commun. ACM 54(7),
pp. 68–76.
Available at http://doi.acm.org/10.1145/1965724.1965743.
F. Bancilhon, D. Maier, Y. Sagiv & J. Ullman (1986):
Magic Sets and other strange ways to implement logic programs.
In: Proceedings of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems.
Available at http://dx.doi.org/10.1145/6012.15399.
F. Benoy & A. King (1996):
Inferring Argument Size Relationships with CLP(R).
In: J. P. Gallagher: Logic-Based Program Synthesis and Transformation (LOPSTR'96),
Springer-Verlag Lecture Notes in Computer Science 1207,
pp. 204–223.
Available at http://dx.doi.org/10.1007/3-540-62718-9_12.
D. Beyer (2013):
Second Competition on Software Verification - (Summary of SV-COMP 2013).
In: N. Piterman & S. A. Smolka: TACAS,
Lecture Notes in Computer Science 7795.
Springer,
pp. 594–609.
Available at http://dx.doi.org/10.1007/978-3-642-36742-7_43.
D. Beyer, T. A. Henzinger, R. Majumdar & A. Rybalchenko (2007):
Path invariants.
In: J. Ferrante & K. S. McKinley: PLDI.
ACM,
pp. 300–309.
Available at http://doi.acm.org/10.1145/1250734.1250769.
N. Bjørner, K. L. McMillan & A. Rybalchenko (2013):
On Solving Universally Quantified Horn Clauses.
In: F. Logozzo & M. Fähndrich: SAS,
Lecture Notes in Computer Science 7935.
Springer,
pp. 105–125.
Available at http://dx.doi.org/10.1007/978-3-642-38856-9_8.
R. Blanc, A. Gupta, L. Kovács & B. Kragl (2013):
Tree Interpolation in Vampire.
In: K. L. McMillan, A. Middeldorp & A. Voronkov: LPAR,
Lecture Notes in Computer Science 8312.
Springer,
pp. 173–181.
Available at http://dx.doi.org/10.1007/978-3-642-45221-5_13.
F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García & G. Puebla (1997):
The Ciao Prolog system. Reference manual.
Technical Report CLIP3/97.1.
School of Computer Science, Technical University of Madrid (UPM).
Available from http://www.clip.dia.fi.upm.es/.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2003):
Counterexample-guided abstraction refinement for symbolic model checking.
J. ACM 50(5),
pp. 752–794.
Available at http://doi.acm.org/10.1145/876638.876643.
P. Cousot & R. Cousot (1977):
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.
In: R. M. Graham, M. A. Harrison & R. Sethi: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977.
ACM,
pp. 238–252.
Available at http://dl.acm.org/citation.cfm?id=512950.
P. Cousot & N. Halbwachs (1978):
Automatic Discovery of Linear Restraints Among Variables of a Program.
In: A. V. Aho, S. N. Zilles & T. G. Szymanski: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978.
ACM Press,
pp. 84–96.
Available at http://dl.acm.org/citation.cfm?id=512760.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
Program verification via iterated specialization.
Sci. Comput. Program. 95,
pp. 149–175.
Available at http://dx.doi.org/10.1016/j.scico.2014.05.017.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
VeriMAP: A Tool for Verifying Programs through Transformations.
In: E. Ábrahám & K. Havelund: TACAS,
Lecture Notes in Computer Science 8413.
Springer,
pp. 568–574.
Available at http://dx.doi.org/10.1007/978-3-642-54862-8_47.
S. Debray & R. Ramakrishnan (1994):
Abstract Interpretation of Logic Programs Using Magic Transformations.
Journal of Logic Programming 18,
pp. 149–176.
Available at http://dx.doi.org/10.1016/0743-1066(94)90050-7.
F. Fioravanti, A. Pettorossi & M. Proietti (2002):
Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs.
In: In Proc. IEEE Conference on Systems, Man and Cybernetics, Hammamet.
IEEE Press.
Available at http://dx.doi.org/10.1109/ICSMC.2002.1167971.
F. Fioravanti, A. Pettorossi, M. Proietti & V. Senni (2013):
Controlling Polyvariance for Specialization-based Verification.
Fundam. Inform. 124(4),
pp. 483–502.
Available at http://dx.doi.org/10.3233/FI-2013-845.
J. P. Gallagher & L. Lafave (1996):
Regular Approximation of Computation Paths in Logic and Functional Languages.
In: O. Danvy, R. Glück & P. Thiemann: Partial Evaluation,
Springer-Verlag Lecture Notes in Computer Science 1110,
pp. 115–136.
Available at http://dx.doi.org/10.1007/3-540-61580-6_7.
G. Gange, J. A. Navas, P. Schachte, H. Søndergaard & P. J. Stuckey (2013):
Failure tabled constraint logic programming by interpolation.
TPLP 13(4-5),
pp. 593–607.
Available at http://dx.doi.org/10.1017/S1471068413000379.
S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea & A. Rybalchenko (2012):
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution).
In: C. Flanagan & B. König: TACAS,
LNCS 7214.
Springer,
pp. 549–551.
Available at http://dx.doi.org/10.1007/978-3-642-28756-5_46.
A. Gupta, C. Popeea & A. Rybalchenko (2011):
Solving Recursion-Free Horn Clauses over LI+UIF.
In: H. Yang: APLAS,
Lecture Notes in Computer Science 7078.
Springer,
pp. 188–203.
Available at http://dx.doi.org/10.1007/978-3-642-25318-8_16.
A. Gupta & A. Rybalchenko (2009):
InvGen: An Efficient Invariant Generator.
In: A. Bouajjani & O. Maler: CAV,
Lecture Notes in Computer Science 5643.
Springer,
pp. 634–640.
Available at http://dx.doi.org/10.1007/978-3-642-02658-4_48.
N. Halbwachs, Y. E. Proy & P. Raymound (1994):
Verification of Linear hybrid systems by means of convex approximations.
In: Proceedings of the First Symposium on Static Analysis,
LNCS 864,
pp. 223–237.
Available at http://dx.doi.org/10.1007/3-540-58485-4_43.
J. Jaffar, V. Murali, J. A. Navas & A. E. Santosa (2012):
TRACER: A Symbolic Execution Tool for Verification.
In: P. Madhusudan & S. A. Seshia: CAV,
Lecture Notes in Computer Science 7358.
Springer,
pp. 758–766.
Available at http://dx.doi.org/10.1007/978-3-642-31424-7_61.
J. Jaffar, J. A. Navas & A. E. Santosa (2011):
Unbounded Symbolic Execution for Program Verification.
In: S. Khurshid & K. Sen: RV,
Lecture Notes in Computer Science 7186.
Springer,
pp. 396–411.
Available at http://dx.doi.org/10.1007/978-3-642-29860-8_32.
L. Lakhdar-Chaouch, B. Jeannet & A. Girault (2011):
Widening with Thresholds for Programs with Complex Control Graphs.
In: T. Bultan & P.-A. Hsiung: ATVA 2011,
Lecture Notes in Computer Science 6996.
Springer,
pp. 492–502.
Available at http://dx.doi.org/10.1007/978-3-642-24372-1_38.
M. Leuschel & T. Massart (1999):
Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
In: A. Bossi: LOPSTR'99,
Lecture Notes in Computer Science 1817.
Springer,
pp. 62–81.
Available at http://dx.doi.org/10.1007/10720327_5.
A. Pettorossi & M. Proietti (2000):
Perfect Model Checking via Unfold/Fold Transformations.
In: J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv & P. J. Stuckey: Computational Logic,
Lecture Notes in Computer Science 1861.
Springer,
pp. 613–628.
Available at http://dx.doi.org/10.1007/3-540-44957-4_41.
A. Rybalchenko & V. Sofronie-Stokkermans (2010):
Constraint solving for interpolation.
J. Symb. Comput. 45(11),
pp. 1212–1233.
Available at http://dx.doi.org/10.1016/j.jsc.2010.06.005.