default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDKenneth L. McMillan
Person information
- affiliation: University of Texas Austin, Austin, USA
- affiliation: Microsoft Research, Redmond, USA
- award (1998): Paris Kanellakis Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j22]Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan:
Invariant Checking for SMT-Based Systems with Quantifiers. ACM Trans. Comput. Log. 25(4): 1-37 (2024)- [c100]Kenneth L. McMillan:
Toward Liveness Proofs at Scale. CAV (1) 2024: 255-276 - [c99]Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen:
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. ICLR 2024 - [i9]Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan:
Invariant Checking for SMT-based Systems with Quantifiers. CoRR abs/2402.19028 (2024) - 2023
- [j21]Orr Tamir
, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv:
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. 7(OOPSLA2): 1878-1904 (2023) - [c98]Yang Hu, Wenxi Wang, Sarfraz Khurshid, Kenneth L. McMillan, Mohit Tiwari:
Fixing Privilege Escalations in Cloud Access Control with MaxSAT and Graph Neural Networks. ASE 2023: 104-115 - [c97]Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck:
A Formal Analysis of Karn's Algorithm. NETYS 2023: 43-61 - [c96]Cole Vick, Kenneth L. McMillan:
Synthesizing History and Prophecy Variables for Symbolic Model Checking. VMCAI 2023: 320-340 - [c95]Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck:
A Case Study in Analytic Protocol Analysis in ACL2. ACL2 2023: 50-66 - [i8]Swen Jacobs, Kenneth L. McMillan, Roopsha Samanta, Ilya Sergey:
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). Dagstuhl Reports 13(3): 32-48 (2023) - 2022
- [j20]Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken:
Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) - [c94]Wenxi Wang, Yang Hu, Kenneth L. McMillan, Sarfraz Khurshid:
SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications. ESEC/SIGSOFT FSE 2022: 1209-1220 - 2021
- [j19]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57(2): 246-269 (2021) - [i7]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR abs/2106.00966 (2021) - [i6]Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen:
NeuroComb: Improving SAT Solving with Graph Neural Networks. CoRR abs/2110.14053 (2021) - 2020
- [c93]Kenneth L. McMillan, Oded Padon:
Ivy: A Multi-modal Verification Tool for Distributed Algorithms. CAV (2) 2020: 190-202 - [i5]Kenneth L. McMillan:
Bayesian Interpolants as Explanations for Neural Inferences. CoRR abs/2004.04198 (2020)
2010 – 2019
- 2019
- [c92]Lenore D. Zuck, Kenneth L. McMillan:
Invisible Invariants Are Neither. From Reactive Systems to Cyber-Physical Systems 2019: 57-72 - [c91]Kenneth L. McMillan, Lenore D. Zuck:
Compositional Testing of Internet Protocols. SecDev 2019: 161-174 - [c90]Kenneth L. McMillan, Lenore D. Zuck:
Formal specification and testing of QUIC. SIGCOMM 2019: 227-240 - 2018
- [c89]Kenneth L. McMillan:
Eager Abstraction for Symbolic Model Checking. CAV (1) 2018: 191-208 - [c88]Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan:
Learning Abstractions for Program Synthesis. CAV (1) 2018: 407-426 - [c87]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD 2018: 1-11 - [c86]Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos:
Modularity for decidability of deductive verification with applications to distributed systems. PLDI 2018: 662-677 - [c85]Kenneth L. McMillan, Oded Padon:
Deductive Verification in Decidable Fragments with Ivy. SAS 2018: 43-55 - [c84]Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf:
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. VMCAI 2018: 336-357 - [p1]Kenneth L. McMillan:
Interpolation and Model Checking. Handbook of Model Checking 2018: 421-446 - [i4]Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan:
Learning Abstractions for Program Synthesis. CoRR abs/1804.04152 (2018) - 2017
- [j18]Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv:
Synthesis of circular compositional program proofs via abduction. Int. J. Softw. Tools Technol. Transf. 19(5): 535-547 (2017) - 2016
- [c83]Kenneth L. McMillan:
Modular specification and verification of a cache-coherent interface. FMCAD 2016: 109-116 - [c82]Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham:
Ivy: safety verification by interactive generalization. PLDI 2016: 614-630 - 2015
- [c81]Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c80]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96 - [i3]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR abs/1508.01288 (2015) - 2014
- [j17]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. ACM SIGPLAN Notices 49(4S): 79-91 (2014) - [c79]Kenneth L. McMillan:
Lazy Annotation Revisited. CAV 2014: 243-259 - [c78]Lenore D. Zuck, Kenneth L. McMillan:
Reasoning about Network Topologies in Space. FPS@ETAPS 2014: 267-277 - [e3]Kenneth L. McMillan, Aart Middeldorp, Geoff Sutcliffe, Andrei Voronkov:
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings. EPiC Series in Computing 26, EasyChair 2014 [contents] - [e2]Kenneth L. McMillan, Xavier Rival:
Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Lecture Notes in Computer Science 8318, Springer 2014, ISBN 978-3-642-54012-7 [contents] - 2013
- [c77]Aws Albarghouthi, Kenneth L. McMillan:
Beautiful Interpolants. CAV 2013: 313-329 - [c76]Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan:
Inductive invariant generation via abductive inference. OOPSLA 2013: 443-456 - [c75]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125 - [c74]Kenneth L. McMillan:
Deductive Generalization. SBMF 2013: 17 - [c73]Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel:
Differential assertion checking. ESEC/SIGSOFT FSE 2013: 345-355 - [c72]Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv:
Synthesis of Circular Compositional Program Proofs via Abduction. TACAS 2013: 370-384 - [e1]Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Lecture Notes in Computer Science 8312, Springer 2013, ISBN 978-3-642-45220-8 [contents] - [i2]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR abs/1306.5264 (2013) - 2012
- [c71]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR 2012: 3-11 - [c70]Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken:
Minimum Satisfying Assignments for SMT. CAV 2012: 394-409 - [c69]Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes:
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6 - 2011
- [c68]Kenneth L. McMillan:
Interpolants from Z3 proofs. FMCAD 2011: 19-27 - [c67]Kenneth L. McMillan:
Widening and Interpolation. SAS 2011: 1 - [c66]Kenneth L. McMillan, Lenore D. Zuck:
Invisible Invariants and Abstract Interpretation. SAS 2011: 249-262 - 2010
- [c65]Kenneth L. McMillan:
Lazy Annotation for Program Testing and Verification. CAV 2010: 104-118
2000 – 2009
- 2009
- [c64]Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv:
Generalizing DPLL to Richer Logics. CAV 2009: 462-476 - [c63]Kenneth L. McMillan:
What's in Common between Test, Model Checking, and Decision Procedures? FMICS 2009: 35-36 - [c62]Kenneth L. McMillan, Lenore D. Zuck:
Abstract Counterexamples for Non-disjunctive Abstractions. RP 2009: 176-188 - 2008
- [j16]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu:
Automated assumption generation for compositional verification. Formal Methods Syst. Des. 32(3): 285-301 (2008) - [c61]Kenneth L. McMillan:
Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference 2008: 3 - [c60]Kenneth L. McMillan:
Relevance heuristics for program analysis. POPL 2008: 145-146 - [c59]Kenneth L. McMillan:
Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427 - 2007
- [j15]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. 3(4) (2007) - [c58]Kenneth L. McMillan:
Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA 2007: 17-18 - [c57]Ranjit Jhala, Kenneth L. McMillan:
Array Abstractions from Proofs. CAV 2007: 193-206 - [c56]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu:
Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432 - [c55]Nina Amla, Kenneth L. McMillan:
Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419 - [c54]Kenneth L. McMillan:
Interpolants and Symbolic Model Checking. VMCAI 2007: 89-90 - [i1]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CoRR abs/0706.0523 (2007) - 2006
- [c53]Kenneth L. McMillan:
Lazy Abstraction with Interpolants. CAV 2006: 123-136 - [c52]Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck:
Liveness by Invisible Invariants. FORTE 2006: 356-371 - [c51]Ranjit Jhala, Kenneth L. McMillan:
A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473 - 2005
- [j14]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Deciding Global Partial-Order Properties. Formal Methods Syst. Des. 26(1): 7-25 (2005) - [j13]Kenneth L. McMillan:
An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005) - [c50]Kenneth L. McMillan:
Applications of Craig Interpolation to Model Checking. ICATPN 2005: 15-16 - [c49]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51 - [c48]Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan:
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. CHARME 2005: 254-268 - [c47]Kenneth L. McMillan:
Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12 - 2004
- [c46]Kenneth L. McMillan:
Applications of Craig Interpolation to Model Checking. CSL 2004: 22-23 - [c45]Nina Amla, Kenneth L. McMillan:
A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274 - [c44]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. POPL 2004: 232-244 - [c43]Kenneth L. McMillan:
An Interpolating Theorem Prover. TACAS 2004: 16-30 - 2003
- [c42]Kenneth L. McMillan:
Interpolation and SAT-Based Model Checking. CAV 2003: 1-13 - [c41]Kenneth L. McMillan:
Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135- - [c40]Kenneth L. McMillan:
Craig Interpolation and Reachability Analysis. SAS 2003: 336 - [c39]Kenneth L. McMillan, Nina Amla:
Automatic Abstraction without Counterexamples. TACAS 2003: 2-17 - [c38]Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel:
Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48 - 2002
- [c37]Kenneth L. McMillan:
Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264 - 2001
- [j12]Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli:
Theory of latency-insensitive design. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(9): 1059-1076 (2001) - [c36]Ranjit Jhala, Kenneth L. McMillan:
Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410 - [c35]Kenneth L. McMillan:
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195 - 2000
- [j11]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160(1-2): 167-188 (2000) - [j10]Kenneth L. McMillan:
A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1-3): 279-309 (2000) - [j9]Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan:
Sibling-substitution-based BDD minimization using don't cares. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 19(1): 44-55 (2000) - [c34]Kenneth L. McMillan, Shaz Qadeer, James B. Saxe:
Induction in Compositional Model Checking. CAV 2000: 312-327 - [c33]Kenneth L. McMillan:
Some Strategies for Proving Theorems with a Model Checker. LICS 2000: 305-306
1990 – 1999
- 1999
- [c32]Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli:
Latency Insensitive Protocols. CAV 1999: 123-133 - [c31]Kenneth L. McMillan:
Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234 - [c30]Kenneth L. McMillan:
Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345 - [c29]Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli:
A methodology for correct-by-construction latency insensitive design. ICCAD 1999: 309-315 - [c28]Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton:
Probabilistic state space search. ICCAD 1999: 574-579 - 1998
- [c27]Kenneth L. McMillan:
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121 - [c26]Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi:
Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450 - [c25]Kenneth L. McMillan:
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD 1998: 1 - [c24]Kenneth L. McMillan:
Proof Rules for Model Checking Systems with Data. FSTTCS 1998: 270 - [c23]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Deciding Global Partial-Order Properties. ICALP 1998: 41-52 - 1997
- [j8]Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang:
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods Syst. Des. 10(2/3): 137-148 (1997) - [c22]Kenneth L. McMillan:
A Compositional Rule for Hardware Design Refinement. CAV 1997: 24-35 - [c21]Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan:
Safe BDD Minimization Using Don't Cares. DAC 1997: 208-213 - 1996
- [c20]Kenneth L. McMillan:
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25 - [c19]Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen:
Symbolic Model Checking. CAV 1996: 419-427 - [c18]Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli:
Engineering Change in a Non-Deterministic FSM Setting. DAC 1996: 451-456 - [c17]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228 - 1995
- [j7]Kenneth L. McMillan:
A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des. 6(1): 45-65 (1995) - [j6]Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness:
Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods Syst. Des. 6(2): 217-232 (1995) - [j5]Robert P. Kurshan, Kenneth L. McMillan:
A Structural Induction Theorem for Processes. Inf. Comput. 117(1): 1-11 (1995) - [c16]Kenneth L. McMillan:
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195 - [c15]Ásgeir Th. Eiríksson, Kenneth L. McMillan:
Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. CAV 1995: 367-380 - [c14]Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao:
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432 - [c13]Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia:
Fast discrete function evaluation using decision diagrams. ICCAD 1995: 402-407 - 1994
- [j4]Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill:
Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4): 401-424 (1994) - [c12]Kenneth L. McMillan:
Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54 - [c11]Kenneth L. McMillan:
Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319 - [c10]Ronald Collett, Mike Gianfagna, Michel Courtoy, Martin Baynes, Johan Van Ginderdeuren, Kenneth L. McMillan, Stephen Ricca, Alberto L. Sangiovanni-Vincentelli, Steve Sapiro, Naeem Zafar:
Panel: Complex System Verification: The Challenge Ahead. DAC 1994: 320 - 1993
- [b1]Kenneth L. McMillan:
Symbolic model checking. Kluwer 1993, ISBN 978-0-7923-9380-1, pp. I-XV, 1-194 - [c9]Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness:
Verification of the Futurebus+ Cache Coherence Protocol. CHDL 1993: 15-30 - [c8]Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang:
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC 1993: 54-60 - 1992
- [j3]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang:
Symbolic Model Checking: 10^20 States and Beyond. Inf. Comput. 98(2): 142-170 (1992) - [c7]Kenneth L. McMillan:
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. CAV 1992: 164-177 - [c6]Kenneth L. McMillan, David L. Dill:
Algorithms for Interface Timing Verification. ICCD 1992: 48-51 - 1991
- [j2]Edmund M. Clarke, David E. Long, Kenneth L. McMillan:
A language for compositional specification and verification of finite state hardware controllers. Proc. IEEE 79(9): 1283-1292 (1991) - [j1]Robert P. Kurshan, Kenneth L. McMillan:
Analysis of digital circuits through symbolic reduction. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 10(11): 1356-1371 (1991) - [c5]Janaki Akella, Kenneth L. McMillan:
Synthesizing Converters Between Finite State Protocols. ICCD 1991: 410-413 - 1990
- [c4]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill:
Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51 - [c3]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang:
Symbolic Model Checking: 10^20 States and Beyond. LICS 1990: 428-439
1980 – 1989
- 1989
- [c2]Edmund M. Clarke, David E. Long, Kenneth L. McMillan:
Compositional Model Checking. LICS 1989: 353-362 - [c1]Robert P. Kurshan, Kenneth L. McMillan:
A Structural Induction Theorem for Processes. PODC 1989: 239-247
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 21:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
