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 × 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 DBLP: McMillan:Kenneth_L=

Facilitated 1 volumes:

VMCAI 2014Ed

Contributed to:

CAV 20142014
CAV 20132013
ESEC/FSE 20132013
OOPSLA 20132013
SAS 20132013
TACAS 20132013
CAV 20122012
SMT 20122012
SAS 20112011
CAV 20102010
CAV 20092009
POPL 20082008
TACAS 20082008
CAV 20072007
TACAS 20072007
VMCAI 20072007
CAV 20062006
TACAS 20062006
CAV 20052005
TACAS 20052005
CSL 20042004
POPL 20042004
TACAS 20042004
CAV 20032003
SAS 20032003
TACAS 20032003
CAV 20022002
CAV 20012001
CAV 20002000
LICS 20002000
CAV 19991999
CAV 19981998
DAC 19981998
ICALP 19981998
CAV 19971997
DAC 19971997
CAV 19961996
DAC 19961996
LICS 19961996
CAV 19951995
DAC 19951995
CAV 19941994
DAC 19941994
DAC 19931993
CAV 19921992
DAC 19901990
LICS 19901990
LICS 19891989
CAV (1) 20182018
PLDI 20162016
PLDI 20182018

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.

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.