BibSLEIGH — Kenneth_L

Travelled to:

1 × Belgium
1 × Germany
1 × Hungary
1 × Israel
1 × Portugal
1 × Spain
2 × Austria
2 × Canada
2 × Denmark
2 × Poland
2 × Russia
21 × USA
3 × France
4 × Italy
4 × United Kingdom

Collaborated with:

∅ R.Jhala E.M.Clarke N.Amla I.Dillig M.Sagiv T.Dillig J.R.Burch N.Bjørner A.Rybalchenko R.Alur D.Peled A.Albarghouthi L.D.Zuck A.L.Sangiovanni-Vincentelli Á.T.Eiríksson B.Li X.Zhao D.L.Dill A.Kuehlmann A.Gupta Z.Fu S.Qadeer J.B.Saxe L.P.Carloni D.E.Long O.Padon S.Shoham S.K.Lahiri R.Sharma C.Hawblitzel A.Aiken T.A.Henzinger R.Majumdar R.P.Kurshan R.Medel K.Ravi T.R.Shiple F.Somenzi Y.Hong P.A.Beerel S.V.A.Campos V.Hartonas-Garmhausen O.Grumberg X.W.0006 G.Anderson M.Fujita J.Yang L.J.Hwang A.Panda S.P.Khatri A.Narayan S.C.Krishnan R.K.Brayton Marcelo Taube G.Losa J.R.Wilcox D.Woos

Talks about:

model (20) check (20) interpol (11) verif (11) abstract (8) symbol (8) composit (7) use (6) program (5) applic (5)

Person: Kenneth L. McMillan

DBLP: McMillan:Kenneth_L=

Facilitated 1 volumes:

Contributed to:

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1990

1989

2018

2016

2018

Wrote 57 papers:

CAV-2014-McMillan #lazy evaluation #revisited: Lazy Annotation Revisited (KLM), pp. 243–259.
CAV-2013-AlbarghouthiM: Beautiful Interpolants (AA, KLM), pp. 313–329.
ESEC-FSE-2013-LahiriMSH #difference: Differential assertion checking (SKL, KLM, RS, CH), pp. 345–355.
OOPSLA-2013-DilligDLM #abduction #generative #induction #invariant: Inductive invariant generation via abductive inference (ID, TD, BL, KLM), pp. 443–456.
SAS-2013-BjornerMR #horn clause #on the #quantifier: On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.
TACAS-2013-LiDDMS #abduction #composition #proving #synthesis: Synthesis of Circular Compositional Program Proofs via Abduction (BL, ID, TD, KLM, MS), pp. 370–384.
CAV-2012-DilligDMA #smt: Minimum Satisfying Assignments for SMT (ID, TD, KLM, AA), pp. 394–409.
SMT-2012-BjornerMR #modulo theories #satisfiability #verification: Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
SAS-2011-McMillan: Widening and Interpolation (KLM), p. 1.
SAS-2011-McMillanZ #abstract interpretation #invariant: Invisible Invariants and Abstract Interpretation (KLM, LDZ), pp. 249–262.
CAV-2010-McMillan #lazy evaluation #testing #verification: Lazy Annotation for Program Testing and Verification (KLM), pp. 104–118.
CAV-2009-McMillanKS #logic: Generalizing DPLL to Richer Logics (KLM, AK, MS), pp. 462–476.
POPL-2008-McMillan #heuristic #program analysis: Relevance heuristics for program analysis (KLM), pp. 145–146.
TACAS-2008-McMillan #generative #invariant #proving #quantifier #using: Quantified Invariant Generation Using an Interpolating Saturation Prover (KLM), pp. 413–427.
CAV-2007-GuptaMF #automation #composition #generative #verification: Automated Assumption Generation for Compositional Verification (AG, KLM, ZF), pp. 420–432.
CAV-2007-JhalaM #abstraction #array #proving: Array Abstractions from Proofs (RJ, KLM), pp. 193–206.
TACAS-2007-AmlaM #abstraction #model checking #refinement #satisfiability: Combining Abstraction Refinement and SAT-Based Model Checking (NA, KLM), pp. 405–419.
VMCAI-2007-McMillan #model checking: Interpolants and Symbolic Model Checking (KLM), pp. 89–90.
CAV-2006-McMillan #abstraction #lazy evaluation: Lazy Abstraction with Interpolants (KLM), pp. 123–136.
TACAS-2006-JhalaM #approach #refinement: A Practical and Complete Approach to Predicate Refinement (RJ, KLM), pp. 459–473.
CAV-2005-JhalaM #approximate: Interpolant-Based Transition Relation Approximation (RJ, KLM), pp. 39–51.
TACAS-2005-McMillan #model checking: Applications of Craig Interpolants in Model Checking (KLM), pp. 1–12.
CSL-2004-McMillan #model checking: Applications of Craig Interpolation to Model Checking (KLM), pp. 22–23.
POPL-2004-HenzingerJMM #abstraction #proving: Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.
TACAS-2004-McMillan #proving #theorem proving: An Interpolating Theorem Prover (KLM), pp. 16–30.
CAV-2003-McMillan #model checking #satisfiability: Interpolation and SAT-Based Model Checking (KLM), pp. 1–13.
SAS-2003-McMillan #analysis #reachability: Craig Interpolation and Reachability Analysis (KLM), p. 336.
TACAS-2003-AmlaKMM #analysis #bound #model checking: Experimental Analysis of Different Techniques for Bounded Model Checking (NA, RPK, KLM, RM), pp. 34–48.
TACAS-2003-McMillanA #abstraction #automation: Automatic Abstraction without Counterexamples (KLM, NA), pp. 2–17.
CAV-2002-McMillan #bound #model checking #satisfiability: Applying SAT Methods in Unbounded Symbolic Model Checking (KLM), pp. 250–264.
CAV-2001-JhalaM #architecture #composition #model checking #verification: Microarchitecture Verification by Compositional Model Checking (RJ, KLM), pp. 396–410.
CAV-2000-McMillanQS #composition #induction #model checking: Induction in Compositional Model Checking (KLM, SQ, JBS), pp. 312–327.
LICS-2000-McMillan #model checking #proving #theorem: Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
CAV-1999-CarloniMS #latency #protocol: Latency Insensitive Protocols (LPC, KLM, ALSV), pp. 123–133.
CAV-1998-McMillan #algorithm #composition #implementation #model checking #verification: Verification of an Implementation of Tomasulo’s Algorithm by Compositional Model Checking (KLM), pp. 110–121.
DAC-1998-RaviMSS #approximate #composition #diagrams: Approximation and Decomposition of Binary Decision Diagrams (KR, KLM, TRS, FS), pp. 445–450.
ICALP-1998-AlurMP #partial order: Deciding Global Partial-Order Properties (RA, KLM, DP), pp. 41–52.
CAV-1997-McMillan #composition #design #hardware #refinement: A Compositional Rule for Hardware Design Refinement (KLM), pp. 24–35.
DAC-1997-HongBBM #using: Safe BDD Minimization Using Don’t Cares (YH, PAB, JRB, KLM), pp. 208–213.
CAV-1996-ClarkeMCH #model checking: Symbolic Model Checking (EMC, KLM, SVAC, VHG), pp. 419–427.
CAV-1996-McMillan #model checking #representation: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (KLM), pp. 13–25.
DAC-1996-KhatriNKMBS #automaton #nondeterminism: Engineering Change in a Non-Deterministic FSM Setting (SPK, AN, SCK, KLM, RKB, ALSV), pp. 451–456.
LICS-1996-AlurMP #concurrent #correctness #model checking: Model-Checking of Correctness Conditions for Concurrent Objects (RA, KLM, DP), pp. 219–228.
CAV-1995-EirikssonM #analysis #case study #design #using #verification: Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study (ÁTE, KLM), pp. 367–380.
CAV-1995-McMillan #using #verification: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings (KLM), pp. 180–195.
DAC-1995-ClarkeGMZ #generative #model checking #performance: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (EMC, OG, KLM, XZ), pp. 427–432.
CAV-1994-McMillan #model checking: Hierarchical Representations of Discrete Functions, with Application to Model Checking (KLM), pp. 41–54.
DAC-1994-McMillan #design #formal method: Fitting Formal Methods into the Design Cycle (KLM), pp. 314–319.
DAC-1993-ClarkeMZFY #scalability: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (EMC, KLM, XZ, MF, JY), pp. 54–60.
CAV-1992-McMillan #explosion #problem #using #verification: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits (KLM), pp. 164–177.
DAC-1990-BurchCMD #model checking #using #verification: Sequential Circuit Verification Using Symbolic Model Checking (JRB, EMC, KLM, DLD), pp. 46–51.
LICS-1990-BurchCMDH #model checking: Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.
LICS-1989-ClarkeLM #composition #model checking: Compositional Model Checking (EMC, DEL, KLM), pp. 353–362.
CAV-2018-McMillan #abstraction #model checking: Eager Abstraction for Symbolic Model Checking (KLM), pp. 191–208.
CAV-2018-WangADM #abstraction #learning #synthesis: Learning Abstractions for Program Synthesis (XW0, GA, ID, KLM), pp. 407–426.
PLDI-2016-PadonMPSS #interactive #named #safety #verification: Ivy: safety verification by interactive generalization (OP, KLM, AP, MS, SS), pp. 614–630.
PLDI-2018-TaubeLMPSSWW #composition #decidability #deduction #distributed #verification: Modularity for decidability of deductive verification with applications to distributed systems (MT, GL, KLM, OP, MS, SS, JRW, DW), pp. 662–677.