BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Cyprus
1 × Finland
1 × India
1 × Ireland
1 × Russia
18 × USA
2 × Japan
2 × Poland
2 × Portugal
2 × Spain
3 × Austria
3 × Canada
3 × The Netherlands
4 × Denmark
4 × Germany
6 × France
6 × United Kingdom
7 × Italy
Collaborated with:
A.Rybalchenko J.Hoenicke W.Charatonik M.Heizmann T.Wies D.Dietsch S.Mukhopadhyay B.Cook A.Farzan Z.Kincaid J.Niehren M.Wehrle A.Post G.Smolka P.V.Roy B.Westphal S.Arlt J.Esparza G.Delzanno H.Aït-Kaci A.Nutz S.Kupferschmid A.Malkis T.Ball S.K.Rajamani E.Ermis S.Wagner B.Musa R.Dimitrova B.Blanchet P.Péladeau M.Schäf C.Herrera I.Menzel N.D.Jones E.Olderog M.N.Seghir I.Schaefer A.Pnueli J.Talbot M.Müller A.Ayari D.A.Basin S.C.Goldstein R.Treinen M.M.0001 R.Majumdar V.Langenfeld T.Morciniec M.M.Mohamed P.Borromeo S.F.Arenis B.Nebel J.Christ M.Lindenmann C.Schilling J.Leike K.R.M.Leino A.Gotsman M.Y.Vardi V.Kuncak P.Lam M.C.Rinard D.A.McAllester D.Niwinski I.Walukiewicz S.Bogomolov G.Frehse R.Grosu H.Ladan O.Padon G.Losa M.Sagiv S.Shoham K.Dräger J.Hoffmann B.Finkbeiner H.Dierks G.Behrmann S.Wissert
Talks about:
program (15) model (14) check (14) abstract (12) constraint (11) analysi (11) termin (11) base (10) logic (8) set (8)

Person: Andreas Podelski

DBLP DBLP: Podelski:Andreas

Facilitated 3 volumes:

PPDP 2007Ed
VMCAI 2007Ed
TACAS 2004Ed

Contributed to:

CAV 20152015
ICST 20152015
LATA 20152015
POPL 20152015
TACAS 20152015
CAV 20142014
ISSTA 20142014
POPL 20142014
TACAS 20142014
CAV 20132013
POPL 20132013
TACAS 20132013
VMCAI 20132013
CAV 20122012
ICTSS 20122012
VMCAI 20122012
FASE 20112011
FM 20112011
RE 20112011
REFSQ 20112011
TACAS 20112011
POPL 20102010
SAS 20102010
TACAS 20102010
FM 20092009
SAS 20092009
TACAS 20092009
CAV 20082008
VMCAI 20082008
PADL 20072007
PLDI 20072007
POPL 20072007
SAS 20072007
TACAS 20072007
CAV 20062006
PLDI 20062006
VMCAI 20062006
ESOP 20052005
POPL 20052005
SAS 20052005
TACAS 20052005
LICS 20042004
VMCAI 20042004
FoSSaCS 20032003
VMCAI 20032003
ICLP 20022002
TACAS 20022002
VMCAI 20022002
PADL 20012001
TACAS 20012001
CL 20002000
POPL 20002000
SAS 20002000
CSL 19991999
ESOP 19991999
TACAS 19991999
LICS 19981998
RTA 19981998
SAS 19981998
TACAS 19981998
CSL 19971997
ILPS 19971997
LICS 19971997
ICLP 19951995
ILPS 19941994
ILPS 19931993
RTA 19931993
ICALP 19921992
PLILP 19911991
ESEC/FSE 20172017
TAPSOFT CAAP/FASE 19931993
TAPSOFT CAAP/FASE 19971997
POPL 20172017
POPL 20182018

Wrote 86 papers:

CAV-2015-DietschHLP #approach #ltl #model checking #modulo theories
Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
ICST-2015-ArltMPW #dependence #testing
If A Fails, Can B Still Succeed? Inferring Dependencies between Test Results in Automotive System Testing (SA, TM, AP, SW), pp. 1–10.
LATA-2015-FarzanHHKP #automation #verification
Automated Program Verification (AF, MH, JH, ZK, AP), pp. 25–46.
POPL-2015-FarzanKP #bound #parallel #proving
Proof Spaces for Unbounded Parallelism (AF, ZK, AP), pp. 407–420.
TACAS-2015-HeizmannDLMP #array #contest
Ultimate Automizer with Array Interpolation — (Competition Contribution) (MH, DD, JL, BM, AP), pp. 455–457.
TACAS-2015-NutzDMP #contest #memory management #safety
ULTIMATE KOJAK with Memory Safety Checks — (Competition Contribution) (AN, DD, MMM, AP), pp. 458–460.
CAV-2014-HeizmannHP #analysis #learning #source code #termination
Termination Analysis by Learning Terminating Programs (MH, JH, AP), pp. 797–813.
ISSTA-2014-ArltPW #slicing #testing #user interface
Reducing GUI test suites via program slicing (SA, AP, MW), pp. 270–281.
POPL-2014-FarzanKP #proving
Proofs that count (AF, ZK, AP), pp. 151–164.
TACAS-2014-ErmisNDHP #contest
Ultimate Kojak — (Competition Contribution) (EE, AN, DD, JH, AP), pp. 421–423.
TACAS-2014-HeizmannCDHLMSWP #contest #satisfiability
Ultimate Automizer with Unsatisfiable Cores — (Competition Contribution) (MH, JC, DD, JH, ML, BM, CS, SW, AP), pp. 418–420.
TACAS-2014-HerreraWP #network #query #reduction
Quasi-Equal Clock Reduction: More Networks, More Queries (CH, BW, AP), pp. 295–309.
CAV-2013-HeizmannHP #automaton #model checking #people
Software Model Checking for People Who Love Automata (MH, JH, AP), pp. 36–52.
POPL-2013-FarzanKP #data flow #graph #induction
Inductive data flow graphs (AF, ZK, AP), pp. 129–142.
TACAS-2013-HeizmannCDEHLNSP #contest
Ultimate Automizer with SMTInterpol — (Competition Contribution) (MH, JC, DD, EE, JH, ML, AN, CS, AP), pp. 641–643.
VMCAI-2013-Podelski #automaton #proving
Automata as Proofs (AP), pp. 13–14.
CAV-2012-BogomolovFGLPW #analysis #distance #reachability
A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx (SB, GF, RG, HL, AP, MW), pp. 479–494.
ICTSS-2012-ArltBSP #testing #user interface
Parameterized GUI Tests (SA, PB, MS, AP), pp. 247–262.
VMCAI-2012-ErmisHP
Splitting via Interpolants (EE, JH, AP), pp. 186–201.
FASE-2011-PostHP #named #realtime #requirements
rt-Inconsistency: A New Property for Real-Time Requirements (AP, JH, AP), pp. 34–49.
FM-2011-DietschWP #verification
System Verification through Program Verification (DD, BW, AP), pp. 27–41.
RE-2011-DietschAWP #ambiguity #formal method #industrial #standard #visual notation
Disambiguation of industrial standards through formalization and graphical languages (DD, SFA, BW, AP), pp. 265–270.
RE-2011-PostHP #realtime #requirements
Vacuous real-time requirements (AP, JH, AP), pp. 153–162.
REFSQ-2011-PostMP #case study #requirements #strict
Applying Restricted English Grammar on Automotive Requirements — Does it Work? A Case Study (AP, IM, AP), pp. 166–180.
TACAS-2011-PodelskiR #abstraction #invariant #termination
Transition Invariants and Transition Predicate Abstraction for Program Termination (AP, AR), pp. 3–10.
POPL-2010-HeizmannHP
Nested interpolants (MH, JH, AP), pp. 471–482.
POPL-2010-PodelskiW
Counterexample-guided focus (AP, TW), pp. 249–260.
SAS-2010-HeizmannJP #invariant #termination
Size-Change Termination and Transition Invariants (MH, NDJ, AP), pp. 22–50.
SAS-2010-MalkisPR #abstraction #refinement #thread
Thread-Modular Counterexample-Guided Abstraction Refinement (AM, AP, AR), pp. 356–372.
TACAS-2010-HoenickeOP
Fairness for Dynamic Control (JH, ERO, AP), pp. 251–265.
FM-2009-HoenickeLPSW
It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.
SAS-2009-HeizmannHP #abstraction #refinement
Refinement of Trace Abstraction (MH, JH, AP), pp. 69–85.
SAS-2009-SeghirPW #abstraction #array #quantifier #refinement
Abstraction Refinement for Quantified Array Assertions (MNS, AP, TW), pp. 3–18.
TACAS-2009-WehrleKP #model checking
Transition-Based Directed Model Checking (MW, SK, AP), pp. 186–200.
CAV-2008-KupferschmidWNP #performance #question
Faster Than Uppaal? (SK, MW, BN, AP), pp. 552–555.
CAV-2008-PodelskiRW
Heap Assumptions on Demand (AP, AR, TW), pp. 314–327.
VMCAI-2008-DimitrovaP #abstraction #lazy evaluation #protocol #question
Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? (RD, AP), pp. 98–111.
PADL-2007-PodelskiR #abstraction #logic #model checking #named #refinement
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement (AP, AR), pp. 245–259.
PLDI-2007-CookPR #concurrent #proving #termination #thread
Proving thread termination (BC, AP, AR), pp. 320–330.
POPL-2007-CookGPRV #proving #source code
Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
SAS-2007-MalkisPR #precise #thread #verification
Precise Thread-Modular Verification (AM, AP, AR), pp. 218–232.
TACAS-2007-KupferschmidDHFDPB #heuristic #model checking
Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking (SK, KD, JH, BF, HD, AP, GB), pp. 679–682.
CAV-2006-CookPR #named #safety
Terminator: Beyond Safety (BC, AP, AR), pp. 415–418.
PLDI-2006-CookPR #proving #termination
Termination proofs for systems code (BC, AP, AR), pp. 415–426.
VMCAI-2006-WiesKLPR #analysis #constraints
Field Constraint Analysis (TW, VK, PL, AP, MCR), pp. 157–173.
ESOP-2005-PodelskiSW #recursion #source code #summary
Summaries for While Programs with Recursion (AP, IS, SW), pp. 94–107.
POPL-2005-PodelskiR #abstraction #termination
Transition predicate abstraction and fair termination (AP, AR), pp. 132–144.
SAS-2005-CookPR #abstraction #refinement #termination
Abstraction Refinement for Termination (BC, AP, AR), pp. 87–101.
SAS-2005-PodelskiW
Boolean Heaps (AP, TW), pp. 268–283.
TACAS-2005-PnueliPR #analysis
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems (AP, AP, AR), pp. 124–139.
LICS-2004-PodelskiR #invariant
Transition Invariants (AP, AR), pp. 32–41.
VMCAI-2004-PodelskiR #linear #ranking #synthesis
A Complete Method for the Synthesis of Linear Ranking Functions (AP, AR), pp. 239–251.
FoSSaCS-2003-BlanchetP #encryption #protocol #termination #verification
Verification of Cryptographic Protocols: Tagging Enforces Termination (BB, AP), pp. 136–152.
VMCAI-2003-Podelski #abstraction #model checking #refinement
Software Model Checking with Abstraction Refinement (AP), pp. 1–3.
ICLP-2002-CharatonikMP #constraints #infinity #model checking
Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP (WC, SM, AP), pp. 115–129.
TACAS-2002-BallPR #abstraction #model checking #refinement
Relative Completeness of Abstraction Refinement for Software Model Checking (TB, AP, SKR), pp. 158–172.
VMCAI-2002-CharatonikMP #analysis #composition #termination
Compositional Termination Analysis of Symbolic Forward Analysis (WC, SM, AP), pp. 109–125.
PADL-2001-MukhopadhyayP #constraints #database #modelling #similarity
Constraint Database Models Characterizing Timed Bisimilarity (SM, AP), pp. 245–258.
TACAS-2001-BallPR #abstraction #c #model checking #source code
Boolean and Cartesian Abstraction for Model Checking C Programs (TB, AP, SKR), pp. 268–283.
CL-2000-MukhopadhyayP #logic #model checking #process
Model Checking for Timed Logic Processes (SM, AP), pp. 598–612.
POPL-2000-CharatonikPT #program analysis
Paths vs. Trees in Set-Based Program Analysis (WC, AP, JMT), pp. 330–337.
POPL-2000-EsparzaP #algorithm #graph #interprocedural #parallel #performance
Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs (JE, AP), pp. 1–11.
SAS-2000-Podelski #constraints #model checking #theorem proving
Model Checking as Constraint Solving (AP), pp. 22–37.
CSL-1999-DelzannoEP #analysis #constraints #protocol
Constraint-Based Analysis of Broadcast Protocols (GD, JE, AP), pp. 50–66.
ESOP-1999-PodelskiCM #analysis #concurrent #constraints #logic programming #source code
Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs (AP, WC, MM), pp. 177–192.
TACAS-1999-DelzannoP #model checking
Model Checking in CLP (GD, AP), pp. 223–239.
LICS-1998-CharatonikMNPW #calculus #μ-calculus
The Horn μ-calculus (WC, DAM, DN, AP, IW), pp. 58–69.
RTA-1998-CharatonikP #constraints #set
Co-definite Set Constraints (WC, AP), pp. 211–225.
SAS-1998-CharatonikP #logic programming #source code #type inference
Directional Type Inference for Logic Programs (WC, AP), pp. 278–294.
TACAS-1998-CharatonikP #analysis #infinity
Set-Based Analysis of Reactive Infinite-State Systems (WC, AP), pp. 358–375.
CSL-1997-AyariBP #named #specification
LISA: A Specification Language Based on WS2S (AA, DAB, AP), pp. 18–34.
ILPS-1997-Podelski #analysis #logic programming #source code
Set-Based Analysis of Logic Programs and Reactive Logic Programs (AP), pp. 35–36.
LICS-1997-CharatonikP #constraints #set
Set Constraints with Intersection (WC, AP), pp. 362–372.
ICLP-1995-PodelskiS #constraints #logic programming #semantics #source code
Operational Semantics of Constraint Logic Programs with Coroutining (AP, GS), pp. 449–463.
ICLP-1995-PodelskiS95a
Situated Simplification (AP, GS), p. 826.
ILPS-1994-PodelskiR #algorithm #incremental #testing
The Beauty and the Beast Algorithm: Quasi-Linear Incremental Tests of Entailment and Disentailment over Trees (AP, PVR), pp. 359–374.
ILPS-1993-Ait-KaciPG #order #unification
Order-Sorted Feature Theory Unification (HAK, AP, SCG), pp. 506–524.
ILPS-1993-PodelskiR #algorithm
The Beauty and the Beast Algorithm (AP, PVR), p. 653.
RTA-1993-NiehrenPT #constraints #equation #finite
Equational and Membership Constraints for Finite Trees (JN, AP, RT), pp. 106–120.
ICALP-1992-PeladeauP #on the
On Reverse and General Definite Tree Languages (PP, AP), pp. 150–161.
PLILP-1991-Ait-KaciP #towards
Towards a Meaning of LIFE (HAK, AP), pp. 255–274.
ESEC-FSE-2017-DietschHMNP #model checking
Craig vs. Newton in software model checking (DD, MH, BM, AN, AP), pp. 487–497.
TAPSOFT-1993-NiehrenP #automaton #set
Feature Automata and Recognizable Sets of Feature Trees (JN, AP), pp. 356–375.
TAPSOFT-1997-MullerNP #constraints #set
Inclusion Constraints over Non-empty Sets of Trees (MM0, JN, AP), pp. 345–356.
POPL-2017-HoenickeMP #composition #concurrent #thread #verification
Thread modularity at many levels: a pearl in compositional verification (JH, RM, AP), pp. 473–485.
POPL-2018-PadonHLPSS #first-order #liveness #logic #safety
Reducing liveness to safety in first-order logic (OP, JH, GL, AP, MS, SS), p. 33.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.