BibSLEIGH — Andreas

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: Podelski:Andreas

Facilitated 3 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1995

1994

1993

1992

1991

2017

1993

1997

2017

2018

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.