Andreas Podelski

Orcid: 0000-0003-2540-9489

Affiliations:
  • University of Freiburg


According to our database1, Andreas Podelski authored at least 191 papers between 1989 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Commutativity Simplifies Proofs of Parameterized Programs.
Proc. ACM Program. Lang., January, 2024

Ultimate Automizer and the Abstraction of Bitwise Operations - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023
Stratified Commutativity in Verification Algorithms for Concurrent Programs.
Proc. ACM Program. Lang., January, 2023

Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

An Empirical Study of the Intuitive Understanding of a Formal Pattern Language.
Proceedings of the Requirements Engineering: Foundation for Software Quality, 2023

2022
Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version).
Inf. Comput., 2022

Ultimate GemCutter and the Axes of Generalization - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Sound sequentialization for concurrent program verification.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Software Model Checking: 20 Years and Beyond.
Proceedings of the Principles of Systems Design, 2022

2021
Temporal prophecy for proving temporal properties of infinite-state systems.
Formal Methods Syst. Des., 2021

Verification of Concurrent Programs Using Petri Net Unfoldings.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Hanfor: Semantic Requirements Review at Scale.
Proceedings of the Joint Proceedings of REFSQ 2021 Workshops, 2021

Separating Map Variables in a Logic-Based Intermediate Verification Language.
Proceedings of the Networked Systems - 9th International Conference, 2021

A Formal Operational Model of ACT-R: Structure and Behaviour.
Proceedings of the 43th Annual Meeting of the Cognitive Science Society, 2021

2019
Ultimate TreeAutomizer (CHC-COMP Tool Description).
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, 2019

Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages.
CoRR, 2019

On Formal Verification of ACT-R Architectures and Models.
Proceedings of the 41th Annual Meeting of the Cognitive Science Society, 2019

Temporal Planning as Refinement-Based Model Checking.
Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, 2019

2018
Predicate Abstraction for Program Verification.
Proceedings of the Handbook of Model Checking., 2018

Reducing liveness to safety in first-order logic.
Proc. ACM Program. Lang., 2018

A Tree-Based Approach to Data Flow Proofs.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

The Map Equality Domain.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

But does it really do that? Using formal analysis to ensure desirable ACT-R model behaviour.
Proceedings of the 40th Annual Meeting of the Cognitive Science Society, 2018

2017
Refining Trace Abstraction using Abstract Interpretation.
CoRR, 2017

Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Craig vs. Newton in software model checking.
Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

Loop Invariants from Counterexamples.
Proceedings of the Static Analysis - 24th International Symposium, 2017

Thread modularity at many levels: a pearl in compositional verification.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016
Guided search for hybrid systems based on coarse-grained space abstractions.
Int. J. Softw. Tools Technol. Transf., 2016

Ready for testing: ensuring conformance to industrial standards through formal verification.
Formal Aspects Comput., 2016

A Logical Approach to Generating Test Plans.
CoRR, 2016

Adaptive moment closure for parameter inference of biochemical reaction networks.
Biosyst., 2016

Classifying Bugs with Interpolants.
Proceedings of the Tests and Proofs - 10th International Conference, 2016

Ultimate Automizer with Two-track Proofs - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Requirements Defects over a Project Lifetime: An Empirical Analysis of Defect Data from a 5-Year Automotive Project at Bosch.
Proceedings of the Requirements Engineering: Foundation for Software Quality, 2016

Proving Liveness of Parameterized Programs.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

2015
ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Ultimate Automizer with Array Interpolation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

System Testing and Program Verification.
Proceedings of the Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März, 2015

Using the requirements specification to infer the implicit test status of requirements.
Proceedings of the 23rd IEEE International Requirements Engineering Conference, 2015

Proof Spaces for Unbounded Parallelism.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Automated Program Verification.
Proceedings of the Language and Automata Theory and Applications, 2015

If A Fails, Can B Still Succeed? Inferring Dependencies between Test Results in Automotive System Testing.
Proceedings of the 8th IEEE International Conference on Software Testing, 2015

Eliminating spurious transitions in reachability with support functions.
Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015

Fairness Modulo Theory: A New Approach to LTL Software Model Checking.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Fairness for Infinitary Control.
Proceedings of the Correct System Design, 2015

2014
Quasi-Equal Clock Reduction: More Networks, More Queries.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Ultimate Kojak - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Proofs that count.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Reducing GUI test suites via program slicing.
Proceedings of the International Symposium on Software Testing and Analysis, 2014

Verification of GUI Applications: A Black-Box Approach.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2014

Quasi-dependent variables in hybrid automata.
Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2014

Assume-Guarantee Abstraction Refinement Meets Hybrid Systems.
Proceedings of the Hardware and Software: Verification and Testing, 2014

Termination Analysis by Learning Terminating Programs.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Planning as Model Checking in Hybrid Domains.
Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013
Monitoring Student Activity in Collaborative Software Development
CoRR, 2013

Automata as Proofs.
Proceedings of the Verification, 2013

Ultimate Automizer with SMTInterpol - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Abstraction-Based Guided Search for Hybrid Systems.
Proceedings of the Model Checking Software - 20th International Symposium, 2013

Inductive data flow graphs.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Push-Down Automata with Gap-Order Constraints.
Proceedings of the Fundamentals of Software Engineering - 5th International Conference, 2013

Detecting Quasi-equal Clocks in Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2013

Software Model Checking for People Who Love Automata.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Linear Ranking for Linear Lasso Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Automotive behavioral requirements expressed in a specification pattern system: a case study at BOSCH.
Requir. Eng., 2012

Black-Box Verification for GUI Applications
CoRR, 2012

Splitting via Interpolants.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Towards successful subcontracting for software in small to medium-sized enterprises.
Proceedings of the Fifth IEEE International Workshop on Requirements Engineering and Law, 2012

Parameterized GUI Tests.
Proceedings of the Testing Software and Systems, 2012

Lightweight Static Analysis for GUI Testing.
Proceedings of the 23rd IEEE International Symposium on Software Reliability Engineering, 2012

Timed Automata with Disjoint Activity.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

Reducing Quasi-Equal Clocks in Networks of Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Interpolant Automata - (Invited Talk).
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
Automatische Validierung von Anforderungen.
Softwaretechnik-Trends, 2011

Proving program termination.
Commun. ACM, 2011

Transition Invariants and Transition Predicate Abstraction for Program Termination.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Applying Restricted English Grammar on Automotive Requirements - Does it Work? A Case Study.
Proceedings of the Requirements Engineering: Foundation for Software Quality, 2011

Vacuous real-time requirements.
Proceedings of the RE 2011, 19th IEEE International Requirements Engineering Conference, Trento, Italy, August 29 2011, 2011

Disambiguation of industrial standards through formalization and graphical languages.
Proceedings of the RE 2011, 19th IEEE International Requirements Engineering Conference, Trento, Italy, August 29 2011, 2011

Composing Stability Proofs for Hybrid Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

System Verification through Program Verification.
Proceedings of the FM 2011: Formal Methods, 2011

rt-Inconsistency: A New Property for Real-Time Requirements.
Proceedings of the Fundamental Approaches to Software Engineering, 2011

2010
Doomed program points.
Formal Methods Syst. Des., 2010

Fairness for Dynamic Control.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Thread-Modular Counterexample-Guided Abstraction Refinement.
Proceedings of the Static Analysis - 17th International Symposium, 2010

Size-Change Termination and Transition Invariants.
Proceedings of the Static Analysis - 17th International Symposium, 2010

Counterexample-guided focus.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Nested interpolants.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Shape-based Barrier Estimation for RNAs.
Proceedings of the German Conference on Bioinformatics 2010, 2010

Explicit Fair Scheduling for Dynamic Control.
Proceedings of the Concurrency, 2010

Composing Reachability Analyses of Hybrid Systems for Safety and Stability.
Proceedings of the Automated Technology for Verification and Analysis, 2010

2009
Directed model checking with distance-preserving abstractions.
Int. J. Softw. Tools Technol. Transf., 2009

Summarization for termination: no return!
Formal Methods Syst. Des., 2009

Transition-Based Directed Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Abstraction Refinement for Quantified Array Assertions.
Proceedings of the Static Analysis, 16th International Symposium, 2009

Refinement of Trace Abstraction.
Proceedings of the Static Analysis, 16th International Symposium, 2009

It's Doomed; We Can Prove It.
Proceedings of the FM 2009: Formal Methods, 2009

2008
Verification, Least-Fixpoint Checking, Abstraction.
Proceedings of the Verified Software: Theories, 2008

Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?
Proceedings of the Verification, 2008

Heap Assumptions on Demand.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Faster Than Uppaal?
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Useless Actions Are Useful.
Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling, 2008

2007
Transition predicate abstraction and fair termination.
ACM Trans. Program. Lang. Syst., 2007

SFB/TR 14 AVACS - Automatic Verification and Analysis of Complex Systems (Der Sonderforschungsbereich/Transregio 14 AVACS - Automatische Verifikation und Analyse komplexer Systeme).
it Inf. Technol., 2007

Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

ACSAR: Software Model Checking with Transfinite Refinement.
Proceedings of the Model Checking Software, 2007

Precise Thread-Modular Verification.
Proceedings of the Static Analysis, 14th International Symposium, 2007

Proving that programs eventually do something good.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Proving thread termination.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement.
Proceedings of the Practical Aspects of Declarative Languages, 9th International Symposium, 2007

A Sound and Complete Proof Rule for Region Stability of Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Region Stability Proofs for Hybrid Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

2006
Tools and algorithms for the construction and analysis of systems.
Int. J. Softw. Tools Technol. Transf., 2006

On Verifying Complex Properties using Symbolic Shape Analysis
CoRR, 2006

Field Constraint Analysis.
Proceedings of the Verification, 2006

Termination proofs for systems code.
Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 2006

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL.
Proceedings of the Model Checking and Artificial Intelligence, 4th Workshop, 2006

Thread-Modular Verification Is Cartesian Abstract Interpretation.
Proceedings of the Theoretical Aspects of Computing, 2006

Model Checking of Hybrid Systems: From Reachability Towards Stability.
Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

Terminator: Beyond Safety.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
Special issue.
Theor. Comput. Sci., 2005

Verification of cryptographic protocols: tagging enforces termination.
Theor. Comput. Sci., 2005

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Boolean Heaps.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Abstraction Refinement for Termination.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Summaries for While Programs with Recursion.
Proceedings of the Programming Languages and Systems, 2005

2004
Introduction to the Special Issue on Verification and Computational Logic.
Theory Pract. Log. Program., 2004

A Complete Method for the Synthesis of Linear Ranking Functions.
Proceedings of the Verification, 2004

Transition Invariants.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Constraints in Program Analysis and Verification.
Proceedings of the Principles and Practice of Constraint Programming, 2004

2003
Boolean and Cartesian abstraction for model checking C programs.
Int. J. Softw. Tools Technol. Transf., 2003

Software Model Checking with Abstraction Refinement.
Proceedings of the Verification, 2003

2002
Set Constraints with Intersection.
Inf. Comput., 2002

Compositional Termination Analysis of Symbolic Forward Analysis.
Proceedings of the Verification, 2002

Relative Completeness of Abstraction Refinement for Software Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

An Algebraic Framework for Abstract Model Checking.
Proceedings of the Abstraction, 2002

Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP.
Proceedings of the Logic Programming, 18th International Conference, 2002

2001
Constraint-based deductive model checking.
Int. J. Softw. Tools Technol. Transf., 2001

Model Checking Communication Protocols.
Proceedings of the SOFSEM 2001: Theory and Practice of Informatics, 28th Conference on Current Trends in Theory and Practice of Informatics Piestany, Slovak Republic, November 24, 2001

Constraint Database Models Characterizing Timed Bisimilarity.
Proceedings of the Practical Aspects of Declarative Languages, 2001

Accurate Widenings and Boundedness Properties of Timed Systems.
Proceedings of the Perspectives of System Informatics, 2001

2000
Ordering Constraints over Feature Trees.
Constraints An Int. J., 2000

Model Checking as Constraint Solving.
Proceedings of the Static Analysis, 7th International Symposium, 2000

Efficient Algorithms for pre<sup>*</sup> and post<sup>*</sup> on Interprocedural Parallel Flow Graphs.
Proceedings of the POPL 2000, 2000

Paths vs. Trees in Set-Based Program Analysis.
Proceedings of the POPL 2000, 2000

Model Checking for Timed Logic Processes.
Proceedings of the Computational Logic, 2000

1999
Model Checking in CLP.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Verification of Infinite-State Systems in Constraint Logic Programming.
Proceedings of the JFPLC'99, 1999

Beyond Region Graphs: Symbolic Forward Analysis of Timed Automata.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1999

Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs.
Proceedings of the Programming Languages and Systems, 1999

Constraint-Based Analysis of Broadcast Protocols.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998
Set-Based Analysis of Reactive Infinite-State Systems.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Directional Type Inference for Logic Programs.
Proceedings of the Static Analysis, 5th International Symposium, 1998

Co-definite Set Constraints.
Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

The Horn Mu-calculus.
Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

1997
Situated Simplification.
Theor. Comput. Sci., 1997

Minimal Ascending and Descending Tree Automata.
SIAM J. Comput., 1997

Order Sorted Feature Theory Unification.
J. Log. Program., 1997

Inclusion Constraints over Non-empty Sets of Trees.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Set-Based Analysis of Logic Programs and Reactive Logic Programs (Abstract).
Proceedings of the Logic Programming, 1997

LISA: A Specification Language Based on WS2S.
Proceedings of the Computer Science Logic, 11th International Workshop, 1997

Set Constraints: A Pearl in Research on Constraints.
Proceedings of the Principles and Practice of Constraint Programming - CP97, Third International Conference, Linz, Austria, October 29, 1997

1996
The Independence Property of a Class of Set Constraints.
Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, 1996

1995
Operational Semantics of Constraint Logic Programs with Coroutining.
Proceedings of the Logic Programming, 1995

A Detailed Algorithm Testing Guards over Feature Trees.
Proceedings of the Constraint Processing, Selected Papers, 1995

1994
Functions as Passive Constraints in LIFE.
ACM Trans. Program. Lang. Syst., 1994

Rabin Tree Automata and Finite Monoids.
Theor. Comput. Sci., 1994

A Feature Constraint System for Logic Programming with Entailment.
Theor. Comput. Sci., 1994

The Beauty and the Beast Algorithm: Quasi-Linear Incremental Tests of Entailment and Disentailment over Trees.
Proceedings of the Logic Programming, 1994

1993
Towards a Meaning of LIFE.
J. Log. Program., 1993

Another variation on the common subexpression problem.
Discret. Math., 1993

Feature Automata and Recognizable Sets of Feature Trees.
Proceedings of the TAPSOFT'93: Theory and Practice of Software Development, 1993

The Beauty and the Beast Algorithm.
Proceedings of the Logic Programming, 1993

Equational and Membership Constraints for Finite Trees.
Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Ultimately Periodic Words of Rational <i>w</i>-Languages.
Proceedings of the Mathematical Foundations of Programming Semantics, 1993

Entailment and Disentailment of Order-Sorted Feature Constraints.
Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

The Beauty and the Beast Algorithm: Testing Entailment and Disentailment Incrementally.
Proceedings of the ICLP'93 Post-Conference Workshop on Concurrent Constraint Programming, 1993

An Informal Introduction to LIFE.
Proceedings of the ICLP'93 Post-Conference Workshop on Concurrent Constraint Programming, 1993

1992
On Reverse and General Definite Tree Languages (Extended Abstract).
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

A Feature-Based Constraint System for Logic Programming with Entailment.
Proceedings of the International Conference on Fifth Generation Computer Systems. FGCS 1992, 1992

Logic Programming with Functions over Order-Sorted Feature Terms.
Proceedings of the Extensions of Logic Programming, Third International Workshop, 1992

A monoid approach to tree automata.
Proceedings of the Tree Automata and Languages., 1992

1991
A Geometrical View of the Determinization and Minimization of Finite-State Automata.
Math. Syst. Theory, 1991

1989
Definite tree languages.
Bull. EATCS, 1989


  Loading...