Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014):
Program verification via iterated specialization.
Science of Computer Programming 95, Part 2,
pp. 149–175,
doi:10.1016/j.scico.2014.05.017.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014):
VeriMAP: A Tool for Verifying Programs through Transformations.
In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014,
Lecture Notes in Computer Science, vol 8413.
Springer,
pp. 568–574,
doi:10.1007/978-3-642-54862-8_47.
Available at: http://www.map.uniroma2.it/VeriMAP.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2015):
A Rule-based Verification Strategy for Array Manipulating Programs.
Fundamenta Informaticae 140(3–4),
pp. 329–355,
doi:10.3233/FI-2015-1257.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2018):
Predicate Pairing for program verification.
Theory and Practice of Logic Programming 18(2),
pp. 126–166,
doi:10.1017/S1471068417000497.
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2017):
Semantics-based generation of verification conditions via program specialization.
Science of Computer Programming 147,
pp. 78–108,
doi:10.1016/j.scico.2016.11.002.
Emanuele D'Osualdo, Jonathan Kochems & C-H Luke Ong (2013):
Automatic verification of Erlang-style concurrency.
In: Proceedings of the 20th International Static Analysis Symposium, SAS 2013,
Lecture Notes in Computer Science, vol 7935.
Springer,
pp. 454–476,
doi:10.1007/978-3-642-38856-9_24.
Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak & Philipp Rümmer (2012):
A Verification Toolkit for Numerical Transition Systems.
In: Proceedings of the 18th International Symposium on Formal Methods, FM 2012,
Lecture Notes in Computer Science, vol 7436.
Springer,
pp. 247–251,
doi:10.1007/978-3-642-32759-9_21.
Jacob M. Howe, Andy King & Lunjin Lu (2004):
Analysing Logic Programs by Reasoning Backwards.
In: Program Development in Computational Logic,
Lecture Notes in Computer Science, vol 3049.
Springer,
pp. 152–188,
doi:10.1007/978-3-540-25951-0_6.
Joxan Jaffar & Michael J. Maher (1994):
Constraint Logic Programming: A Survey.
Journal of Logic Programming 19/20,
pp. 503–581,
doi:10.1016/0743-1066(94)90033-7.
Bishoksan Kafle, John P. Gallagher & José F. Morales (2016):
RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata.
In: Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016,
Lecture Notes in Computer Science, vol 9779.
Springer,
pp. 261–268,
doi:10.1007/978-3-319-41528-4_14.
Bishoksan Kafle, John P. Gallagher, Graeme Gange, Peter Schachte, Harald Søndergaard & Peter J. Stuckey (2018):
An iterative approach to precondition inference using constrained Horn clauses.
CoRR abs/1804.05989.
Available at http://arxiv.org/abs/1804.05989.
Tobias Lindahl & Konstantinos Sagonas (2006):
Practical type inference based on success typings.
In: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, PPDP 2006.
ACM,
pp. 167–178,
doi:10.1145/1140335.1140356.
Leonardo M. de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008,
Lecture Notes in Computer Science, vol 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
Konstantinos Sagonas, Josep Silva & Salvador Tamarit (2013):
Precise explanation of success typing errors.
In: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation, PEPM 2013.
ACM,
pp. 33–42,
doi:10.1145/2426890.2426897.
Robert Virding, Claes Wikström & Mike Williams (1996):
Concurrent Programming in ERLANG (2nd Ed.).
Prentice Hall International (UK) Ltd..
eptcs@eptcs.org