@article(BagnaraHZ08SCP, author = "R. Bagnara and P. M. Hill and E. Zaffanella", year = "2008", title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems", journal = "Science of Computer Programming", volume = "72", number = "1--2", pages = "3--21", url = "http://dx.doi.org/10.1016/j.scico.2007.08.001", ) @article(DBLP:journals/cacm/BallLR11, author = "T. Ball and V. Levin and S. K. Rajamani", year = "2011", title = "A decade of software model checking with SLAM", journal = "Commun. ACM", volume = "54", number = "7", pages = "68--76", url = "http://doi.acm.org/10.1145/1965724.1965743", ) @inproceedings(Bancilhon-Maier-Sagiv-Ullman, author = "F. Bancilhon and D. Maier and Y. Sagiv and J. Ullman", year = "1986", title = "Magic Sets and other strange ways to implement logic programs", booktitle = "Proceedings of the 5$^{th}$ {ACM SIGMOD-SIGACT} Symposium on Principles of Database Systems", url = "http://dx.doi.org/10.1145/6012.15399", ) @inproceedings(Benoy-King-LOPSTR96, author = "F. Benoy and A. King", year = "1996", title = "Inferring Argument Size Relationships with {CLP(R)}", editor = "J. P. Gallagher", booktitle = "Logic-Based Program Synthesis and Transformation (LOPSTR'96)", series = "Springer-Verlag Lecture Notes in Computer Science", volume = "1207", pages = "204--223", url = "http://dx.doi.org/10.1007/3-540-62718-9_12", ) @inproceedings(DBLP:conf/tacas/Beyer13, author = "D. Beyer", year = "2013", title = "Second Competition on Software Verification - (Summary of SV-COMP 2013)", editor = "N. Piterman and S. A. Smolka", booktitle = "TACAS", series = "Lecture Notes in Computer Science", volume = "7795", publisher = "Springer", pages = "594--609", url = "http://dx.doi.org/10.1007/978-3-642-36742-7_43", ) @inproceedings(DBLP:conf/pldi/BeyerHMR07, author = "D. Beyer and T. A. Henzinger and R. Majumdar and A. Rybalchenko", year = "2007", title = "Path invariants", editor = "J. Ferrante and K. S. McKinley", booktitle = "PLDI", publisher = "ACM", pages = "300--309", url = "http://doi.acm.org/10.1145/1250734.1250769", ) @inproceedings(DBLP:conf/sas/BjornerMR13, author = "N. Bj{\o }rner and K. L. McMillan and A. Rybalchenko", year = "2013", title = "On Solving Universally Quantified Horn Clauses", editor = "F. Logozzo and M. F{\"a}hndrich", booktitle = "SAS", series = "Lecture Notes in Computer Science", volume = "7935", publisher = "Springer", pages = "105--125", url = "http://dx.doi.org/10.1007/978-3-642-38856-9_8", ) @inproceedings(DBLP:conf/lpar/BlancGKK13, author = "R. Blanc and A. Gupta and L. Kov{\'a}cs and B. Kragl", year = "2013", title = "Tree Interpolation in Vampire", editor = "K. L. McMillan and A. Middeldorp and A. Voronkov", booktitle = "LPAR", series = "Lecture Notes in Computer Science", volume = "8312", publisher = "Springer", pages = "173--181", url = "http://dx.doi.org/10.1007/978-3-642-45221-5_13", ) @techreport(ciao-reference-manual-tr, author = "F. Bueno and D. Cabeza and M. Carro and M. Hermenegildo and P. L\'{o}pez-Garc\'{\i }a and G. Puebla", year = "1997", title = "The {C}iao {P}rolog system. Reference manual", type = "Technical Report", number = "{CLIP}3/97.1", institution = "School of Computer Science, Technical University of Madrid (UPM)", note = "Available from http://www.clip.dia.fi.upm.es/", ) @article(DBLP:journals/jacm/ClarkeGJLV03, author = "E. M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith", year = "2003", title = "Counterexample-guided abstraction refinement for symbolic model checking", journal = "J. ACM", volume = "50", number = "5", pages = "752--794", url = "http://doi.acm.org/10.1145/876638.876643", ) @inproceedings(DBLP:conf/popl/CousotC77, author = "P. Cousot and R. Cousot", year = "1977", title = "Abstract Interpretation: {A} Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints", editor = "R. M. Graham and M. A. Harrison and R. Sethi", booktitle = "Conference Record of the Fourth {ACM} Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977", publisher = "{ACM}", pages = "238--252", url = "http://dl.acm.org/citation.cfm?id=512950", ) @inproceedings(DBLP:conf/popl/CousotH78, author = "P. Cousot and N. Halbwachs", year = "1978", title = "Automatic Discovery of Linear Restraints Among Variables of a Program", editor = "A. V. Aho and S. N. Zilles and T. G. Szymanski", booktitle = "Conference Record of the Fifth Annual {ACM} Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978", publisher = "{ACM} Press", pages = "84--96", url = "http://dl.acm.org/citation.cfm?id=512760", ) @article(DBLP:journals/scp/AngelisFPP14, author = "E. {De Angelis} and F. Fioravanti and A. Pettorossi and M. Proietti", year = "2014", title = "Program verification via iterated specialization", journal = "Sci. Comput. Program.", volume = "95", pages = "149--175", url = "http://dx.doi.org/10.1016/j.scico.2014.05.017", ) @inproceedings(DBLP:conf/tacas/AngelisFPP14, author = "E. De Angelis and F. Fioravanti and A. Pettorossi and M. Proietti", year = "2014", title = "VeriMAP: A Tool for Verifying Programs through Transformations", editor = "E. {\'A}brah{\'a}m and K. Havelund", booktitle = "TACAS", series = "Lecture Notes in Computer Science", volume = "8413", publisher = "Springer", pages = "568--574", url = "http://dx.doi.org/10.1007/978-3-642-54862-8_47", ) @article(Debray-Ramakrishnan-94, author = "S. Debray and R. Ramakrishnan", year = "1994", title = "{A}bstract {I}nterpretation of {L}ogic {P}rograms {U}sing {M}agic {T}ransformations", journal = "Journal of Logic Programming", volume = "18", pages = "149--176", url = "http://dx.doi.org/10.1016/0743-1066(94)90050-7", ) @inproceedings(Fioravanti02specializationwith, author = "F. Fioravanti and A. Pettorossi and M. Proietti", year = "2002", title = "Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs", booktitle = "In Proc. IEEE Conference on Systems, Man and Cybernetics, Hammamet", publisher = "IEEE Press", url = "http://dx.doi.org/10.1109/ICSMC.2002.1167971", ) @article(DBLP:journals/fuin/FioravantiPPS13, author = "F. Fioravanti and A. Pettorossi and M. Proietti and V. Senni", year = "2013", title = "Controlling Polyvariance for Specialization-based Verification", journal = "Fundam. Inform.", volume = "124", number = "4", pages = "483--502", url = "http://dx.doi.org/10.3233/FI-2013-845", ) @inproceedings(Gallagher-Lafave-Dagstuhl, author = "J. P. Gallagher and L. Lafave", year = "1996", title = "Regular Approximation of Computation Paths in Logic and Functional Languages", editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", booktitle = "Partial Evaluation", series = "Springer-Verlag Lecture Notes in Computer Science", volume = "1110", pages = "115--136", url = "http://dx.doi.org/10.1007/3-540-61580-6\_7", ) @article(DBLP:journals/tplp/GangeNSSS13, author = "G. Gange and J. A. Navas and P. Schachte and H. S{\o }ndergaard and P. J. Stuckey", year = "2013", title = "Failure tabled constraint logic programming by interpolation", journal = "TPLP", volume = "13", number = "4-5", pages = "593--607", url = "http://dx.doi.org/10.1017/S1471068413000379", ) @inproceedings(DBLP:conf/tacas/GrebenshchikovGLPR12, author = "S. Grebenshchikov and A. Gupta and N. P. Lopes and C. Popeea and A. Rybalchenko", year = "2012", title = "HSF(C): A Software Verifier Based on {H}orn Clauses - (Competition Contribution)", editor = "C. Flanagan and B. K{\"o}nig", booktitle = "TACAS", series = "LNCS", volume = "7214", publisher = "Springer", pages = "549--551", url = "http://dx.doi.org/10.1007/978-3-642-28756-5_46", ) @inproceedings(DBLP:conf/aplas/GuptaPR11, author = "A. Gupta and C. Popeea and A. Rybalchenko", year = "2011", title = "Solving Recursion-Free Horn Clauses over LI+UIF", editor = "H. Yang", booktitle = "APLAS", series = "Lecture Notes in Computer Science", volume = "7078", publisher = "Springer", pages = "188--203", url = "http://dx.doi.org/10.1007/978-3-642-25318-8_16", ) @inproceedings(DBLP:conf/cav/GuptaR09, author = "A. Gupta and A. Rybalchenko", year = "2009", title = "InvGen: An Efficient Invariant Generator", editor = "A. Bouajjani and O. Maler", booktitle = "CAV", series = "Lecture Notes in Computer Science", volume = "5643", publisher = "Springer", pages = "634--640", url = "http://dx.doi.org/10.1007/978-3-642-02658-4_48", ) @inproceedings(Halbwachs-94, author = "N. Halbwachs and Y. E. Proy and P. Raymound", year = "1994", title = "Verification of Linear hybrid systems by means of convex approximations", booktitle = "Proceedings of the First Symposium on Static Analysis", series = "LNCS", volume = "864", pages = "223--237", url = "http://dx.doi.org/10.1007/3-540-58485-4\_43", ) @article(JaffarM94, author = "J. Jaffar and M. Maher", year = "1994", title = "{C}onstraint {L}ogic {P}rogramming: {A} {S}urvey", journal = "Journal of Logic Programming", volume = "19/20", pages = "503--581", url = "http://dx.doi.org/10.1016/0743-1066(94)90033-7", ) @inproceedings(DBLP:conf/cav/JaffarMNS12, author = "J. Jaffar and V. Murali and J. A. Navas and A. E. Santosa", year = "2012", title = "TRACER: A Symbolic Execution Tool for Verification", editor = "P. Madhusudan and S. A. Seshia", booktitle = "CAV", series = "Lecture Notes in Computer Science", volume = "7358", publisher = "Springer", pages = "758--766", url = "http://dx.doi.org/10.1007/978-3-642-31424-7_61", ) @inproceedings(DBLP:conf/rv/JaffarNS11, author = "J. Jaffar and J. A. Navas and A. E. Santosa", year = "2011", title = "Unbounded Symbolic Execution for Program Verification", editor = "S. Khurshid and K. Sen", booktitle = "RV", series = "Lecture Notes in Computer Science", volume = "7186", publisher = "Springer", pages = "396--411", url = "http://dx.doi.org/10.1007/978-3-642-29860-8_32", ) @inproceedings(Lakhdar-ChaouchJG11, author = "L. Lakhdar-Chaouch and B. Jeannet and A. Girault", year = "2011", title = "Widening with Thresholds for Programs with Complex Control Graphs", editor = "T. Bultan and P.-A. Hsiung", booktitle = "ATVA 2011", series = "Lecture Notes in Computer Science", volume = "6996", publisher = "Springer", pages = "492--502", url = "http://dx.doi.org/10.1007/978-3-642-24372-1\_38", ) @inproceedings(LeuschelM99, author = "M. Leuschel and T. Massart", year = "1999", title = "Infinite State Model Checking by Abstract Interpretation and Program Specialisation", editor = "A. Bossi", booktitle = "LOPSTR'99", series = "Lecture Notes in Computer Science", volume = "1817", publisher = "Springer", pages = "62--81", url = "http://dx.doi.org/10.1007/10720327\_5", ) @article(Levi00, author = "G. Levi", year = "2000", title = "Abstract Interpretation Based Verification of Logic Programs", journal = "Electr. Notes Theor. Comput. Sci.", volume = "40", pages = "243", url = "http://dx.doi.org/10.1016/S1571-0661(05)80052-0", ) @inproceedings(PettorossiP00, author = "A. Pettorossi and M. Proietti", year = "2000", title = "Perfect Model Checking via Unfold/Fold Transformations", editor = "J. W. Lloyd and V. Dahl and U. Furbach and M. Kerber and K.-K. Lau and C. Palamidessi and L. M. Pereira and Y. Sagiv and P. J. Stuckey", booktitle = "Computational Logic", series = "Lecture Notes in Computer Science", volume = "1861", publisher = "Springer", pages = "613--628", url = "http://dx.doi.org/10.1007/3-540-44957-4\_41", ) @article(DBLP:journals/jsc/RybalchenkoS10, author = "A. Rybalchenko and V. Sofronie-Stokkermans", year = "2010", title = "Constraint solving for interpolation", journal = "J. Symb. Comput.", volume = "45", number = "11", pages = "1212--1233", url = "http://dx.doi.org/10.1016/j.jsc.2010.06.005", ) @inproceedings(Winsborough89, author = "W. H. Winsborough", year = "1989", title = "Path-Dependent Reachability Analysis for Multiple Specialization.", editor = "E. L. Lusk and R. A. Overbeek", booktitle = "NACLP", publisher = "MIT Press", pages = "133--153", url = "http://dblp.uni-trier.de/db/conf/slp/slp89.html#Winsborough89", )