@article(abdulla2014optimal, author = {Parosh Abdulla and Stavros Aronis and Bengt Jonsson and Konstantinos Sagonas}, year = {2014}, title = {Optimal dynamic partial order reduction}, journal = {ACM SIGPLAN Notices}, volume = {49}, number = {1}, pages = {373--384}, doi = {10.1145/2535838.2535845}, ) @article(De&14c, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2014}, title = {Program verification via iterated specialization}, journal = {Science of Computer Programming}, volume = {95, Part 2}, pages = {149--175}, doi = {10.1016/j.scico.2014.05.017}, ) @inproceedings(De&14b, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2014}, title = {{V}eri{MAP}: {A} {T}ool for {V}erifying {P}rograms through {T}ransformations}, booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014}, series = {Lecture Notes in Computer Science, vol 8413}, publisher = {Springer}, pages = {568--574}, doi = {10.1007/978-3-642-54862-8\_47}, note = {Available at: \url{http://www.map.uniroma2.it/VeriMAP}}, ) @article(De&15d, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2015}, title = {A Rule-based Verification Strategy for Array Manipulating Programs}, journal = {Fundamenta Informaticae}, volume = {140}, number = {3--4}, pages = {329--355}, doi = {10.3233/FI-2015-1257}, ) @article(De&17c, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2018}, title = {Predicate {P}airing for program verification}, journal = {Theory and Practice of Logic Programming}, volume = {18}, number = {2}, pages = {126--166}, doi = {10.1017/S1471068417000497}, ) @article(de2017semantics, author = {De Angelis, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2017}, title = {Semantics-based generation of verification conditions via program specialization}, journal = {Science of Computer Programming}, volume = {147}, pages = {78--108}, doi = {10.1016/j.scico.2016.11.002}, ) @inproceedings(d2013automatic, author = {Emanuele D'Osualdo and Jonathan Kochems and C-H Luke Ong}, year = {2013}, title = {Automatic verification of Erlang-style concurrency}, booktitle = {Proceedings of the 20th International Static Analysis Symposium, SAS 2013}, series = {Lecture Notes in Computer Science, vol 7935}, publisher = {Springer}, pages = {454--476}, doi = {10.1007/978-3-642-38856-9\_24}, ) @inproceedings(Ho&12, author = {Hossein Hojjat and Filip Konecn{\'y} and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp R{\"u}mmer}, year = {2012}, title = {A Verification Toolkit for Numerical Transition Systems}, booktitle = {Proceedings of the 18th International Symposium on Formal Methods, {FM 2012}}, series = {Lecture Notes in Computer Science, vol 7436}, publisher = {Springer}, pages = {247--251}, doi = {10.1007/978-3-642-32759-9\_21}, ) @article(Ho&04, author = {Jacob M. Howe and Andy King and Lunjin Lu}, year = {2004}, title = {Analysing Logic Programs by Reasoning Backwards}, booktitle = {Program Development in Computational Logic}, series = {Lecture Notes in Computer Science, vol 3049}, publisher = {Springer}, pages = {152--188}, doi = {10.1007/978-3-540-25951-0\_6}, ) @article(JaM94, author = {Joxan Jaffar and Michael J. Maher}, year = {1994}, title = {Constraint Logic Programming: {A} Survey}, journal = {Journal of Logic Programming}, volume = {19/20}, pages = {503--581}, doi = {10.1016/0743-1066(94)90033-7}, ) @inproceedings(Ka&16, author = {Bishoksan Kafle and John P. Gallagher and Jos\'e F. Morales}, year = {2016}, title = {{RAHFT}: {A} Tool for Verifying {H}orn Clauses Using Abstract Interpretation and Finite Tree Automata}, booktitle = {Proceedings of the 28th International Conference on Computer Aided Verification, {CAV} 2016}, series = {Lecture Notes in Computer Science, vol 9779}, publisher = {Springer}, pages = {261--268}, doi = {10.1007/978-3-319-41528-4\_14}, ) @article(Ka&18, author = {Bishoksan Kafle and John P. Gallagher and Graeme Gange and Peter Schachte and S{\o}ndergaard, Harald and Peter J. Stuckey}, year = {2018}, title = {An iterative approach to precondition inference using constrained Horn clauses}, journal = {CoRR}, volume = {abs/1804.05989}, url = {http://arxiv.org/abs/1804.05989}, ) @inproceedings(lindahl2006practical, author = {Tobias Lindahl and Konstantinos Sagonas}, year = {2006}, title = {Practical type inference based on success typings}, booktitle = {Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, PPDP 2006}, organization = {ACM}, pages = {167--178}, doi = {10.1145/1140335.1140356}, ) @inproceedings(DeB08, author = {Leonardo M. de Moura and Bj{\o}rner, Nikolaj}, year = {2008}, title = {Z3: {A}n Efficient {SMT} Solver}, booktitle = {Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS}~2008}, series = {Lecture Notes in Computer Science, vol 4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3\_24}, ) @inproceedings(sagonas2013precise, author = {Konstantinos Sagonas and Josep Silva and Salvador Tamarit}, year = {2013}, title = {Precise explanation of success typing errors}, booktitle = {Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation, PEPM 2013}, organization = {ACM}, pages = {33--42}, doi = {10.1145/2426890.2426897}, ) @book(AWV96, author = {Robert Virding and Claes Wikstr\"{o}m and Mike Williams}, year = {1996}, title = {Concurrent Programming in ERLANG (2nd Ed.)}, publisher = {Prentice Hall International (UK) Ltd.}, )