@InProceedings{PW-HSCC06, author = {Andreas Podelski and Silke Wagner}, title = {Model Checking of Hybrid Systems: From Reachability towards Stability}, booktitle = {Proceedings of HSCC'06: Hybrid Systems: Computation and Control}, year = 2006, editor = {Joao P. Hespanha and Ashish Tiwari}, volume = 3927, series = {LNCS}, publisher = {Springer-Verlag}, pages = {507-521} } @InProceedings{PR-TACAS05, author = {Andreas Podelski and Andrey Rybalchenko}, title = {Fairness and Well-Foundedness}, booktitle = {Proceedings of TACAS'05: Tools and Algorithms for the Construction and Analysis of Systems}, year = 2005, editor = {Nicolas Halbwachs and Lenore Zuck}, volume = 2280, series = {LNCS}, isbn = {3-540-43419-4}, publisher = {Springer-Verlag}, pages = {1--15}, } @InProceedings{PSW-ESOP05, author = {Andreas Podelski and Ina Schaefer and Silke Wagner}, title = {Summaries for Total Correctness of Recursive Programs}, editor = {S. Sagiv}, volume = "1576", series = "LNCS", booktitle = "ESOP'05: European Symposium on Programming", year = 2005, publisher = "Springer-Verlag", pages = {1-15} } @InProceedings{PR-POPL05, author = {Andreas Podelski and Andrey Rybalchenko}, title = {Transition Predicate Abstraction and Fair Termination}, booktitle = {Proceedings of POPL'05: Principles of Programming Languages}, year = 2005, editor = {Martin Abadi}, cmonth = {January}, organization = {ACM}, publisher = {ACM Press}, pages = {1--11} } @InProceedings{PR-LICS04, author = {Andreas Podelski and Andrey Rybalchenko}, title = {Transition Invariants}, booktitle = {LICS'04: Logic in Computer Science}, pages = {32--41}, year = 2004, caddress = {Turku, Finland}, cmonth = {July 13-17}, editor = {Harald Ganzinger}, series = {LNCS}, publisher = {IEEE}, isbn = {0-7695-2192-4} } @InProceedings{P-VMCAI04, author = {Andreas Podelski and Andrey Rybalchenko}, title = {A Complete Method for Synthesis of Linear Ranking Functions}, booktitle = {VMCAI~2003: Verification, Model Checking, and Abstract Interpretation}, pages = {239-251}, year = 2004, editor = {Bernhard Steffen and Giorgio Levi}, volume = 2937, series = {LNCS}, publisher = {Springer}, isbn = {3-540-20803-8} } @InProceedings{BP-Fossacs03, author = {Bruno Blanchet and Andreas Podelski}, title = {Verification of Cryptographic Protocols: Tagging Enforces Termination}, booktitle = {FoSSaCS'03: Foundations of Software Science and Computation Structures}, pages = {136--152}, year = 2003, editor = {Andrew D. Gordon}, volume = 2620, series = {LNCS}, publisher = {Springer}, isbn = {3-540-00897-7} } @InProceedings{P-VMCAI03, author = {Andreas Podelski and Andrey Rybalchenko}, title = {Software Model Checking with Abstraction Refinement}, booktitle = {VMCAI~2004: Verification, Model Checking, and Abstract Interpretation}, pages = {1--13}, year = 2003, editor = {Lenore D. Zuck}, volume = 2575, series = {LNCS}, publisher = {Springer}, isbn = {3-540-00348-7} } @InProceedings{BPR-TACAS02, author = {Thomas Ball and Andreas Podelski and Sriram K. Rajamani}, title = {Relative Completeness of Abstraction Refinement for Software Model Checking}, booktitle = {Proceedings of TACAS02: Tools and Algorithms for the Construction and Analysis of Systems}, year = 2002, editor = {Joost-Pieter Kaoen and Perdita Stevens}, volume = 2280, series = {LNCS}, caddress = {Grenoble, France}, cmonth = {April}, isbn = {3-540-43419-4}, publisher = {Springer-Verlag}, pages = {158--172}, } @InProceedings{MP-SARA02, author = {Supratik Mukhopadhyay and Andreas Podelski}, title = {An Algebraic Framework for Abstract Model Checking}, booktitle = {SARA 2002: 5th International Symposium on Abstraction, Reformulation and Approximation}, pages = {152--169}, year = 2002, editor = {Sven Koenig and Robert C. Holte}, volume = 2371, series = {LNCS}, isbn = {3-540-43941-2}, publisher = {Springer} } @InProceedings{CMP-VMCAI02, author = {Witold Charatonik and Supratik Mukhopadhyay and Andreas Podelski}, title = {Compositional Termination Analysis of Symbolic Forward Analysis}, booktitle = {VMCAI~2002: Verification, Model Checking, and Abstract Interpretation}, pages = {109--125}, year = 2002, editor = {Agostino Cortesi}, volume = 2294, series = {LNCS}, isbn = {3-540-43631-6}, publisher = {Springer} } Article{DP-STTT02, author = {Giorgio Delzanno and Andreas Podelski}, title = {Constraint-based Deductive Model Checking}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, year = 2001, page = {250--270}, volume = 3, number = 3 } @Article{CPintersectionJ, author = {Witold Charatonik and Andreas Podelski}, title = {Set Constraints with Intersection}, journal = {Information and Control}, year = 2002, volume = 170, pages = {1--17} } @InProceedings{argon01:_model_check_commun_protoc, author = {Pablo Argon and Giorgio Delzanno and Supratik Mukhopadhyay and Andreas Podelski}, title = {Model Checking for Communication Protocols}, booktitle = {Proceedings of the 28th Annual Conference on Current Trends in Theory and Practice of Software}, pages = {160--170}, year = 2001, editor = {Leszek Pacholski and Peter Ruzicka}, volume = 2234, confaddress = {Slovak Republic}, confmonth = {November--December}, series = {Lecture Notes in Computer Science}, publisher = {Springer} } @InProceedings{PodelskiSAS00, author = {Andreas Podelski}, title = {Model Checking as Constraint Solving}, booktitle = {Proceedings of SAS: Static Analysis Symposium}, pages = {22-37}, year = 2000, editor = {Jens Palsberg}, volume = 1824, series = {LNCS}, caddress = {Santa Barbara, CA}, cmonth = {June--July}, publisher = {Springer-Verlag} } @Article{BPR-STTT03, author = {Tom Ball and Andreas Podelski and Sriram K. Rajamani}, title = {Boolean and Cartesian Abstraction for Model Checking {C} Programs}, journal = {International Journal on Software Tools for Technology Transfer (STTT), Special Section on TACAS'01}, year = 2003, note = {To appear.} } @InProceedings{BPR-TACAS01, author = {Thomas Ball and Andreas Podelski and Sriram K. Rajamani}, title = {Boolean and {Cartesian} Abstraction for Model Checking {C} Programs}, booktitle = {Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems}, year = 2001, editor = {Tiziana Margaria and Wang Yi}, volume = 2031, series = {LNCS}, caddress = {Genova, Italy}, cmonth = {April}, publisher = {Springer-Verlag}, pages = {268--283}, } @InProceedings{EP-POPL00, author = {Javier Esparza and Andreas Podelski}, title = {Efficient Algorithms for Pre$^\star$ and Post$^\star$ on Interprocedural Parallel Flow Graphs}, booktitle = {Proceedings of POPL'00: Principles of Programming Languages}, year = 2000, editor = {Tom Reps}, cOPTaddress = {Boston}, month = {January}, organization = {ACM}, publisher = {ACM Press}, pages = {1--11}, } @InProceedings{CPT-POPL00, author = {Witold Charatonik and Andreas Podelski and Jean-Marc Talbot}, title = {Paths vs. Trees in Set-based Program Analysis}, booktitle = {Proceedings of POPL'00: Principles of Programming Languages}, year = 2000, editor = {Tom Reps}, cOPTaddress = {Boston}, month = {January}, organization = {ACM}, publisher = {ACM Press}, pages = {330-338}, } @InProceedings{DEP99, author = "Giorgio Delzanno and Javier Esparza and Andreas Podelski", title = "Constraint-Based Analysis of Broadcast Protocols", editor = {J\"org Flum and Mario Rodriguez-Artalejo}, volume = "1683", series = "LNCS", Pages = "50--66", booktitle = "Proceedings of the Computer Science Logic Conference (CSL'99)", year = 1999, publisher = "Springer-Verlag", address = "Berlin, Germany", cmonth = "September 20-25", caddress = {Madrid, Spain} } @InProceedings{MP:TLP, author = {Supratik Mukhopadhyay and Andreas Podelski}, title = {Model Checking for Timed Logical Processes}, booktitle = {Proceedings of CL2000: Computational Logic}, publisher = {Springer-Verlag}, year = 2000, editor = {John Lloyd et~al.}, volume = 1861, series = {LNCS}, address = {Berlin, Germany}, cmonth = "July", caddress = {London, Great Britain}, pages = {1--11}, } @InProceedings{MP99, author = "Supratik Mukhopadhyay and Andreas Podelski", title = "Beyond Region Graphs: Symbolic Forward Analysis for Timed Automata", editor = "C. Pandu Rangan and V. Raman and R. Ramanujam", volume = 1738, series = "LNCS", pages = "232--244", booktitle = "Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS '99)", year = 1999, publisher = "Springer-Verlag", address = "Berlin, Germany", cmonth = "December 13--15", caddress = {Chennai, India} } @Article{MNPorderingJ, author = {Martin M\"uller and Joachim Niehren and Andreas Podelski}, title = {Ordering Constraints over Feature Trees}, journal = "Constraints", pages = {7--41}, year = 1999, volume = 5, number = {1-2} } @InProceedings{diagnosis, author = {Andreas Podelski and Witold Charatonik and Martin M\"uller}, title = "Set-based Failure Analysis for Logic Programs and Concurrent Constraint Programs", editor = "S. Doaitse Swierstra", volume = "1576", series = "LNCS", booktitle = "Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99", year = 1999, publisher = "Springer-Verlag", caddress = "Amsterdam", cmonth = "March 22-26", pages = {177-192} } @InProceedings{DPmcclp, author = "Giorgio Delzanno and Andreas Podelski", title = "Model Checking in {CLP}", editor = "Rance Cleaveland", series = "Springer LNCS", booktitle = "Proceedings of TACAS'99, the Second International Conference on Tools and Algorithms for the Construction and Analysis of Systems", year = 1999, publisher = "Springer-Verlag", caddress = "Amsterdam", cmonth = "March 22--26", volume = 1579, pages = "223--239", } @InProceedings{directionalSAS98, author = "Witold Charatonik and Andreas Podelski", title = "Directional Type Inference for Logic Programs", editor = "Giorgio Levi", series = "Springer LNCS", booktitle = "Proceedings of the International Symposium on Static Analysis (SAS'98), Pisa, September 14 - 16, 1998", year = 1998, publisher = "Springer-Verlag", pages = "278--294", volume = 1503 } @INPROCEEDINGS{CharatonikMNPW-LICS98, AUTHOR = {Charatonik, Witold and McAllester, David and Niwinski, Damian and Podelski, Andreas and Walukiewicz, Igor}, EDITOR = {Pratt, Vaughan}, TITLE = {The Horn Mu-calculus}, BOOKTITLE = {Proceedings Thirteenth Annual IEEE Symposium on Logic in Computer Science}, ORGANIZATION = {IEEE Technical Committee on Mathematical Foundations of Computing}, TYPE = {Extended Abstract}, PADDRESS = {Los Alamitos, USA}, ADDRESS = {Indianapolis, Indiana}, PUBLISHER = {IEEE Computer Society}, MONTH = {June}, ISBN = {0-8186-8506-9}, YEAR = {1998}, PAGES = {58--69}, ABSTRACT = {The Horn $\mu$-calculus is a logic programming language allowing arbitrary nesting of least and greatest fixed points. The Horn $\mu$-programs can naturally expresses safety and liveness properties for reactive systems. We extend the set-based analysis of classical logic programs by mapping arbitrary $\mu$-programs into ``uniform'' $\mu$-programs. Our two main results are that uniform $\mu$-programs express regular sets of trees and that emptiness for uniform $\mu$-programs is EXPTIME-complete. Hence we have a nontrivial decidable relaxation for the Horn $\mu$-calculus. In a different reading, the results express a kind of robustness of the notion of regularity: alternating Rabin tree automata preserve the same expressiveness and algorithmic complexity if we extend them with pushdown transition rules (in the same way B\"uchi extended word automata to canonical systems).}, } % www.mpi-sb.mpg.de/$\tilde{\;}$podelski/papers/HornMuCalculus.ps @Unpublished{CMPDagstuhl, author = "Witold Charatonik and David McAllester and Andreas Podelski", title = "Computing the least and the greatest model of the set-based abstraction of logic programs", note = "Presented at the Dagstuhl Workshop on Tree Automata, October~1997" } @InProceedings{LisaCSL, author = "Abdelwaheb Ayari and David Basin and Andreas Podelski", title = "{LISA}: A Specification Language Based on {WS2S}", editor = "Mogens Nielson and Wolfgang Thomas", series = "LNCS", booktitle = "Proceedings of the Conference for Computer Science Logic - CSL'97", volume = 1414, publisher = "Springer-Verlag", address = "Aarhus, Denmark", month = "August", pages = "18--34", year = 1998 } @InProceedings{CPtacas98, author = "Witold Charatonik and Andreas Podelski", title = "Set-based Analysis of Reactive Infinite-state Systems", booktitle = "Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems", caddress = "Lisbon, Portugal", series = "LNCS", volume = 1384, publisher = "Springer-Verlag", year = 1998, editor = "Bernhard Steffen", cmonth = "March-April", pages = "358--375" } @InProceedings{co-definite, author = "Witold Charatonik and Andreas Podelski", title = "Co-definite Set Constraints", editor = "Tobias Nipkow", series = "LNCS", volume = 1379, booktitle = "Proceedings of the 9th International Conference on Rewriting Techniques and Applications", year = 1998, caddress = "Tsukuba, Japan", publisher = "Springer-Verlag", cmonth = "March-April", pages = "211--225" } @InProceedings{PP:CP97, author = "Leszek Pacholski and Andreas Podelski", title = "Set Constraints - a Pearl in Research on Constraints", editor = "Gert Smolka", volume = 1330, series = "Springer LNCS", booktitle = "Proceedings of the Third International Conference on Principles and Practice of Constraint Programming - CP97", year = 1997, publisher = "Springer-Verlag", month = "October", pages = "549--561" } @InProceedings{ilpsTutorial, author = "Andreas Podelski", title = "Set-based Analysis of Concurrent Programs (Invited Tutorial)", editor = "Jan Ma\l uszy\'nski", pages = "35--36", booktitle = "Proceedings of the 14th International Logic Programming Symposium", publisher = "The MIT~Press", address = "Port Jefferson, NY", year = 1997, month = "October" } @InProceedings{MNP:CP97, author = {Martin M\"uller and Joachim Niehren and Andreas Podelski}, title = {Ordering Constraints over Feature Trees}, editor = "Gert Smolka", series = "LNCS", booktitle = "Proceedings of the Third International Conference on Principles and Practice of Constraint Programming - CP97", year = 1997, publisher = "Springer-Verlag", address = "Berlin, Germany", month = "October", pages = "297--311" } @InProceedings{CharatonikPodelskiLICS97, author = "Witold Charatonik and Andreas Podelski", title = "Set Constraints with Intersection", editor = "Glynn Winskel", booktitle = "Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS)", year = 1997, organization = "IEEE", month = "June", pages = "362--372" } @InProceedings{MNP-Ines, author = {Martin M\"uller and Joachim Niehren and Andreas Podelski}, title = "Inclusion Constraints over Non-empty Sets of Trees", editor = "Michel Bidoit and Max Dauchet", booktitle = "Proceedings of the 4th International Joint Conference on Theory and Practice of Software Development \mbox{(TAPSOFT)}, Lille, France, April 1997.", year = 1997, publisher = "Springer-Verlag, Berlin, Germany", volume = 1214, series = "LNCS", pages = "345--356", } @Unpublished{MNP-Journal, author = {Martin M\"uller and Joachim Niehren and Andreas Podelski}, title = "Nonempty Set Constraints", note = "Extended version of~\cite{MNP-Ines}", year = 1999 } @InProceedings{CharatonikPodelskiCP96, author = "Witold Charatonik and Andreas Podelski", title = "The Independence Property of Inclusion Constraints over Non-empty Sets of Trees", pages = "76--90", editor = "Eugene Freuder", number = 1118, series = "LNCS", booktitle = "Principle and Practice of Constraint Programming - CP96", year = 1996, publisher = "Springer-Verlag, Berlin, Germany", address = "Cambridge, MA", month = "August" } @InProceedings{CP:95, author = {Andreas Podelski and Gert Smolka}, title = {Situated Simplification}, booktitle = {Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP'95)}, year = 1995, month = "19--22 " # sep, editor = "Ugo Montanari", address = {Cassis, France}, publisher = "Springer-Verlag", series = {Lecture Notes in Computer Science}, pages = {328--344} } @InProceedings{PodelskiSmolka95, author = {Andreas Podelski and Gert Smolka}, title = "Operational Semantics of Constraint Logic Programming with Coroutining", booktitle = "Proceedings of the 12th International Conference on Logic Programming", address = "Kanagawa, Japan", month = june, year = 1995, publisher = "The MIT Press", editor = "Leon Sterling", pages = "449--463", } @Article{CP:95TCS, author = "Andreas Podelski and Gert Smolka", title = "Situated Simplification", journal = "Theoretical Computer Science (TCS)", year = 1997, volume = 173, pages = "209--233", month = "February" } @article {FunctionsPassive, author = {Hassan A{\"\i}t-Kaci and Andreas Podelski}, title = "Functions as Passive Constraints in LIFE", journal = "ACM Transactions on Programming Languages and Systems (TOPLAS)", volume = 16, number = 4, month = "July", year = 1994, pages = "1279--1318" } @inproceedings{BeautyBeast, author = {Andreas Podelski and Peter Van Roy}, title = "The {Beauty} and the {Beast} algorithm: Quasi-linear incremental tests of entailment and disentailment", booktitle = "Proceedings of the International Symposium on Logic Programming (ILPS)", editor = "Maurice Bruynooghe", publisher = "MIT Press", month = "November", year = 1994, pages = "359--374" } @Book{Podelski95, title = "Constraint Programming: Basics and Trends", publisher = {Springer-Verlag, Berlin, Germany}, address = {Berlin, Heidelberg, New York}, volume = 910, series = "LNCS", publisher = "Springer-Verlag, Berlin, Germany", month = March, year = 1995, editor = "Andreas Podelski", } @Article{JLP93, author = { Hassan A\"{\i}t-Kaci and Andreas Podelski}, title = {Towards a meaning of {Li}fe}, journal = JLP, volume = {16}, number = {3 and 4}, year = {1993}, month = {July, August}, pages = {195-234} } @Article{FeatureTreesTCS, author = {Hassan A\"{\i}t-Kaci and Andreas Podelski and Gert Smolka}, title = "A feature constraint system for logic programming with entailment", journal = "Theoretical Computer Science (TCS)", year = 1994, volume = 122, pages = "263--283" } @Article{OSF:JLP97, author = {Hassan A\"{\i}t-Kaci and Andreas Podelski and Seth Goldstein}, title = "{OSF}-theory unification", journal = "Journal of Logic Programming (JLP)", year = 1997, volume = 30, number = 2, pages = "99--124", month = "February" } @InProceedings{APlpar93, author = {Hassan A{\"\i}t-Kaci and Andreas Podelski}, title = "Entailment and disentailment of order-sorted feature constraints", booktitle = "Proceedings of the Fourth International Conference on Logic Programming and Automated Reasoning", editor = "Andrei Voronkov", series = "Springer LNAI~698", publisher = "Springer-Verlag, Berlin, Germany", month = "July", year = "1993", pages = "1--18", } @Article{nivatSIAM, author = "Maurice Nivat and Andreas Podelski", title = "Minimal ascending and descending tree automata", journal = "SIAM Journal of Computing (SICOMP)", year = 1997, volume = 26, number = 1, pages = "39--58", month = "February" } @Unpublished{PodVor99, author = "Andreas Podelski and Andrei Voronkov", title = "Nonemptiness of 1-Letter Finite Automata Intersection (Can Concurrent Program Verification be Polynomial?)", note = "In preparation", year = 1999 } @Unpublished{ChaNiwPod99, author = "Witold Charatonik and Damian Niwinski and Andreas Podelski", title = " Model Checking for Uniform Programs", note = "In preparation", year = 1999 } @Unpublished{EspKnoPod99, author = "Javier Esparza and Jens Knoop and Andreas Podelski", title = "An Automata-Theoretic Approach to Interprocedural Dataflow Analysis", note = "In preparation", year = 1999 } @Unpublished{KnoPod99, author = "Jens Knoop and Andreas Podelski", title = "Dataflow Analysis as Infinite-State Model Checking", note = "In preparation", year = 1999 } @Unpublished{ChaEspPod99, author = "Witold Charatonik and Javier Esparza and Andreas Podelski", title = "Global Model Checking for Pushdown Systems", note = "In preparation", year = 1999 } @Unpublished{DelPod99a, author = "Giorgio Delzanno and Andreas Podelski", title = "Verifying Integer-Valued Systems with Constraints over Reals", note = "In preparation", year = 1999 } @Unpublished{DelPod99b, author = "Giorgio Delzanno and Andreas Podelski", title = "Accurate Widenings for Model Checking", note = "In preparation", year = 1999 } @Unpublished{DelPod99b, author = "Giorgio Delzanno and Andreas Podelski", title = "Verifying Liveness Properties with Narrowing", note = "In preparation", year = 1999 } @InProceedings{MP-SARA02, author = {Supratik Mukhopadhyay and Andreas Podelski}, title = {An Algebraic Framework for Abstract Model Checking}, booktitle = {Proceedings of SARA~2002: Symposium on Abstraction, Reformulation and Approximation}, pages = {152--169}, year = 2002, editor = {Sven Koenig and Robert C. Holte}, volume = 2371, series = {LNCS}, address = {Berlin, Heidelberg, New York}, publisher = {Springer}, isbn = {3-540-43941-2} } @InProceedings{CMP-ICLP02, author = {Witold Charatonik and Supratik Mukhopadhyay and Andreas Podelski}, title = {Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP}, booktitle = {ICLP'02: 18th International Conference on Logic Programming}, pages = {115--129}, year = 2002, editor = {Peter J. Stuckey}, volume = 2401, isbn = {3-540-43930-7}, series = {LNCS}, publisher = {Springer} } @InProceedings{MP01, author = {Supratik Mukhopadhyay and Andreas Podelski}, title = {Accurate Widenings and Boundedness Properties of Timed Systems}, editor = {Dines Bj{\o}rner and Manfred Broy and Alexandre V. Zamulin}, booktitle = {Perspectives of System Informatics: 4th International Andrei Ershov Memorial Conference}, journal = {LNCS}, publisher = {Springer}, volume = 2244, pages = {79--94}, isbn = {3-540-43075-X}, confaddress = {Novosibirsk,Russia}, confmonth = {July}, year = 2001, } @InProceedings{MP-PADL01, author = {Supratik Mukhopadhyay and Andreas Podelski}, title = {Constraint Database Models Characterizing Timed Bisimilarity}, booktitle = {Practical Aspects of Declarative Languages, Third International Symposium, PADL 2001, Las Vegas, Nevada, March~2001, Proceedings}, publisher = {Springer}, series = {LNCS}, volume = 1990, pages = {245--258}, year = 2001 }