Ken McMillan's Publications
121 results
2019
[121] Compositional Testing of Network Protocols ( and ), In IEEE Secure Development Conference (SecDev 2019), . [bibtex] [pdf]
[120] Formal specification and testing of QUIC ( and ), In Proceedgins of. ACM Special Interest Group on Data Communication (SIGCOMM’19), ACM, . [bibtex] [pdf]
2018
[119] Interpolation and Model Checking (), Chapter in Handbook of Model Checking., . [bibtex] [pdf] [doi]
[118] Learning Abstractions for Program Synthesis (), In CoRR, volume abs/1804.04152, . [bibtex] [pdf]
[117] P\^5 : Planner-less Proofs of Probabilistic Parameterized Protocols (), In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, . [bibtex] [pdf] [doi]
[116] Deductive Verification in Decidable Fragments with Ivy (), In Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (Andreas Podelski, ed.), Springer, volume 11002, . [bibtex] [pdf] [doi]
[115] Modularity for decidability of deductive verification with applications to distributed systems (), In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, . [bibtex] [pdf] [doi]
[114] Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems (), In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 (Nikolaj Bjørner, Arie Gurfinkel, eds.), IEEE, . [bibtex] [pdf] [doi]
[113] Learning Abstractions for Program Synthesis (), In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Hana Chockler, Georg Weissenbacher, eds.), Springer, volume 10981, . [bibtex] [pdf] [doi]
[112] Eager Abstraction for Symbolic Model Checking (), In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Hana Chockler, Georg Weissenbacher, eds.), Springer, volume 10981, . [bibtex] [pdf] [doi]
2017
[111] Synthesis of circular compositional program proofs via abduction (), In STTT, volume 19, . [bibtex] [pdf] [doi]
2016
[110] Ivy: safety verification by interactive generalization (), In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, . [bibtex] [pdf] [doi]
[109] Modular specification and verification of a cache-coherent interface (), In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, . [bibtex] [pdf] [doi]
2015
[108] Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays (), In CoRR, volume abs/1508.01288, . [bibtex] [pdf]
[107]Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays (), In Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015., . [bibtex]
[106] Horn Clause Solvers for Program Verification (), In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, . [bibtex] [pdf] [doi]
2014
[105] Reasoning about Network Topologies in Space (), In From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings, . [bibtex] [pdf] [doi]
[104] Lazy Annotation Revisited (), In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, . [bibtex] [pdf] [doi]
2013
[103] Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types (), In CoRR, volume abs/1306.5264, . [bibtex] [pdf]
[102] Synthesis of Circular Compositional Program Proofs via Abduction (), In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, . [bibtex] [pdf] [doi]
[101] Differential assertion checking (), In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013, . [bibtex] [pdf] [doi]
[100] Deductive Generalization (), In Formal Methods: Foundations and Applications - 16th Brazilian Symposium, SBMF 2013, Brasilia, Brazil, September 29 - October 4, 2013, Proceedings, . [bibtex] [pdf] [doi]
[99] On Solving Universally Quantified Horn Clauses (), In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, . [bibtex] [pdf] [doi]
[98] Inductive invariant generation via abductive inference (), In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, . [bibtex] [pdf] [doi]
[97] Beautiful Interpolants (), In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, . [bibtex] [pdf] [doi]
2012
[96] Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials (), In Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, . [bibtex] [pdf] [doi]
[95] Minimum Satisfying Assignments for SMT (), In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, . [bibtex] [pdf] [doi]
[94] Program Verification as Satisfiability Modulo Theories (), In 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012, . [bibtex] [pdf]
2011
[93] Invisible Invariants and Abstract Interpretation (), In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, . [bibtex] [pdf] [doi]
[92] Widening and Interpolation (), In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, . [bibtex] [pdf] [doi]
[91] Interpolants from Z3 proofs (), In International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011, . [bibtex] [pdf]
2010
[90] Lazy Annotation for Program Testing and Verification (), In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, . [bibtex] [pdf] [doi]
2009
[89] Abstract Counterexamples for Non-disjunctive Abstractions (), In Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings, . [bibtex] [pdf] [doi]
[88] What's in Common between Test, Model Checking, and Decision Procedures? (), In Formal Methods for Industrial Critical Systems, 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings, . [bibtex] [pdf] [doi]
[87] Generalizing DPLL to Richer Logics (), In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, . [bibtex] [pdf] [doi]
2008
[86] Automated assumption generation for compositional verification (), In Formal Methods in System Design, volume 32, . [bibtex] [pdf] [doi]
[85] Quantified Invariant Generation Using an Interpolating Saturation Prover (), In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, . [bibtex] [pdf] [doi]
[84] Relevance heuristics for program analysis (), In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, . [bibtex] [pdf] [doi]
[83] Proofs, Interpolants, and Relevance Heuristics (), In Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27-30, 2008. Proceedings, . [bibtex] [pdf] [doi]
2007
[82] Interpolant-Based Transition Relation Approximation (), In Logical Methods in Computer Science, volume 3, . [bibtex] [pdf] [doi]
[81] Interpolant-Based Transition Relation Approximation (), In CoRR, volume abs/0706.0523, . [bibtex] [pdf]
[80] Interpolants and Symbolic Model Checking (), In Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings, . [bibtex] [pdf] [doi]
[79] Combining Abstraction Refinement and SAT-Based Model Checking (), In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, . [bibtex] [pdf] [doi]
[78] Array Abstractions from Proofs (), In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, . [bibtex] [pdf] [doi]
[77] Automated Assumption Generation for Compositional Verification (), In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, . [bibtex] [pdf] [doi]
[76] Toward Property-Driven Abstraction for Heap Manipulating Programs (), In Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, . [bibtex] [pdf] [doi]
2006
[75] A Practical and Complete Approach to Predicate Refinement (), In Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings, . [bibtex] [pdf] [doi]
[74] Liveness by Invisible Invariants (), In Formal Techniques for Networked and Distributed Systems - FORTE 2006, 26th IFIP WG 6.1 International Conference, Paris, France, September 26-29, 2006., . [bibtex] [pdf] [doi]
[73] Lazy Abstraction with Interpolants (), In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, . [bibtex] [pdf] [doi]
2005
[72] An interpolating theorem prover (), In Theor. Comput. Sci., volume 345, . [bibtex] [pdf] [doi]
[71] Deciding Global Partial-Order Properties (), In Formal Methods in System Design, volume 26, . [bibtex] [pdf] [doi]
[70] Applications of Craig Interpolants in Model Checking (), In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, . [bibtex] [pdf] [doi]
[69] An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment (), In Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings, . [bibtex] [pdf] [doi]
[68] Interpolant-Based Transition Relation Approximation (), In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, . [bibtex] [pdf] [doi]
[67] Applications of Craig Interpolation to Model Checking (), In Applications and Theory of Petri Nets 2005, 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005, Proceedings, . [bibtex] [pdf] [doi]
2004
[66] An Interpolating Theorem Prover (), In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, . [bibtex] [pdf] [doi]
[65] Abstractions from proofs (), In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, . [bibtex] [pdf] [doi]
[64] A Hybrid of Counterexample-Based and Proof-Based Abstraction (), In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, . [bibtex] [pdf] [doi]
[63] Applications of Craig Interpolation to Model Checking (), In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, . [bibtex] [pdf] [doi]
2003
[62] Automatic Abstraction without Counterexamples (), In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, . [bibtex] [pdf] [doi]
[61] Experimental Analysis of Different Techniques for Bounded Model Checking (), In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, . [bibtex] [pdf] [doi]
[60] Craig Interpolation and Reachability Analysis (), In Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings, . [bibtex] [pdf] [doi]
[59] Methods for exploiting SAT solvers in unbounded model checking (), In 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings, . [bibtex] [pdf] [doi]
[58] Interpolation and SAT-Based Model Checking (), In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, . [bibtex] [pdf] [doi]
2002
[57] Applying SAT Methods in Unbounded Symbolic Model Checking (), In Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, . [bibtex] [pdf] [doi]
2001
[56] Theory of latency-insensitive design (), In IEEE Trans. on CAD of Integrated Circuits and Systems, volume 20, . [bibtex] [pdf] [doi]
[55] Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking (), In Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings, . [bibtex] [pdf] [doi]
[54] Microarchitecture Verification by Compositional Model Checking (), In Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, . [bibtex] [pdf] [doi]
2000
[53] Sibling-substitution-based BDD minimization using don't cares (), In IEEE Trans. on CAD of Integrated Circuits and Systems, volume 19, . [bibtex] [pdf] [doi]
[52] A methodology for hardware verification using compositional model checking (), In Sci. Comput. Program., volume 37, . [bibtex] [pdf] [doi]
[51] Model-Checking of Correctness Conditions for Concurrent Objects (), In Inf. Comput., volume 160, . [bibtex] [pdf] [doi]
[50] Some Strategies for Proving Theorems with a Model Checker (), In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, . [bibtex] [pdf] [doi]
[49] Induction in Compositional Model Checking (), In Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, . [bibtex] [pdf] [doi]
1999
[48] Probabilistic state space search (), In Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999, San Jose, California, USA, November 7-11, 1999, . [bibtex] [pdf] [doi]
[47] A methodology for correct-by-construction latency insensitive design (), In Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999, San Jose, California, USA, November 7-11, 1999, . [bibtex] [pdf] [doi]
[46] Circular Compositional Reasoning about Liveness (), In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings, . [bibtex] [pdf] [doi]
[45] Verification of Infinite State Systems by Compositional Model Checking (), In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings, . [bibtex] [pdf] [doi]
[44] Latency Insensitive Protocols (), In Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings, . [bibtex] [pdf] [doi]
1998
[43] Deciding Global Partial-Order Properties (), In Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings, . [bibtex] [pdf] [doi]
[42] Proof Rules for Model Checking Systems with Data (), In Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings, . [bibtex] [pdf] [doi]
[41] Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract) (), In Formal Methods in Computer-Aided Design, Second International Conference, FMCAD '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings, . [bibtex] [pdf] [doi]
[40] Approximation and Decomposition of Binary Decision Diagrams (), In Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, 1998., . [bibtex] [pdf] [doi]
[39] Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking (), In Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, . [bibtex] [pdf] [doi]
1997
[38] Heuristic symmetry reduction for invariant verification (, and ), In Internaitonal Workshop on Logic Synthesis (IWLS '97), . [bibtex] [pdf]
[37] Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (), In Formal Methods in System Design, volume 10, . [bibtex] [pdf] [doi]
[36] Safe BDD Minimization Using Don't Cares (), In Proceedings of the 34st Conference on Design Automation, Anaheim, California, USA, Anaheim Convention Center, June 9-13, 1997., . [bibtex] [pdf] [doi]
[35] A Compositional Rule for Hardware Design Refinement (), In Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings, . [bibtex] [pdf] [doi]
1996
[34] Model-Checking of Correctness Conditions for Concurrent Objects (), In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, . [bibtex] [pdf] [doi]
[33] Engineering Change in a Non-Deterministic FSM Setting (), In Proceedings of the 33st Conference on Design Automation, Las Vegas, Nevada, USA, Las Vegas Convention Center, June 3-7, 1996., . [bibtex] [pdf] [doi]
[32] A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (), In Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, . [bibtex] [pdf] [doi]
[31] Symbolic Model Checking (), In Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, . [bibtex] [pdf] [doi]
1995
[30] A Structural Induction Theorem for Processes (), In Inf. Comput., volume 117, . [bibtex] [pdf] [doi]
[29] A Technique of State Space Search Based on Unfolding (), In Formal Methods in System Design, volume 6, . [bibtex] [pdf] [doi]
[28] Verification of the Futurebus+ Cache Coherence Protocol (), In Formal Methods in System Design, volume 6, . [bibtex] [pdf] [doi]
[27] Fast discrete function evaluation using decision diagrams (), In Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, November 5-9, 1995, . [bibtex] [pdf] [doi]
[26] Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (), In Proceedings of the 32st Conference on Design Automation, San Francisco, California, USA, Moscone Center, June 12-16, 1995., . [bibtex] [pdf] [doi]
[25] Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings (), In Computer Aided Verification, 7th International Conference, Liège, Belgium, July, 3-5, 1995, Proceedings, . [bibtex] [pdf] [doi]
[24] Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study (), In Computer Aided Verification, 7th International Conference, Liège, Belgium, July, 3-5, 1995, Proceedings, . [bibtex] [pdf] [doi]
1994
[23] Symbolic model checking for sequential circuit verification (), In IEEE Trans. on CAD of Integrated Circuits and Systems, volume 13, . [bibtex] [pdf] [doi]
[22] Fitting Formal Methods into the Design Cycle (), In Proceedings of the 31st Conference on Design Automation, San Diego, California, USA, June 6-10, 1994., . [bibtex] [pdf] [doi]
[21] Panel: Complex System Verification: The Challenge Ahead (), In Proceedings of the 31st Conference on Design Automation, San Diego, California, USA, June 6-10, 1994., . [bibtex] [pdf] [doi]
[20] Hierarchical Representations of Discrete Functions, with Application to Model Checking (), In Computer Aided Verification, 6th International Conference, CAV '94, Stanford, California, USA, June 21-23, 1994, Proceedings, . [bibtex] [pdf] [doi]
1993
[19] Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (), In Proceedings of the 30th Design Automation Conference. Dallas, Texas, USA, June 14-18, 1993., . [bibtex] [pdf] [doi]
[18] Verification of the Futurebus+ Cache Coherence Protocol (), In Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL '93, sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993, . [bibtex] [pdf]
[17]Symbolic model checking (), Kluwer, . [bibtex]
1992
[16] Symbolic Model Checking: an approach to the state explosion problem (), PhD thesis, Carnegie Mellon, . [bibtex] [pdf]
[15] Symbolic Model Checking: 10\^20 States and Beyond (), In Inf. Comput., volume 98, . [bibtex] [pdf] [doi]
[14] Algorithms for Interface Timing Verification (), In Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, ICCD '92, Cambridge, MA, USA, October 11-14, 1992, . [bibtex] [pdf] [doi]
[13] Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits (), In Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings, . [bibtex] [pdf] [doi]
[12]Automatic verification of sequential circuit designs (, , , and ), In Philosophical Transactions of the Royal Society, Series A, . [bibtex]
1991
[11] Formal verification of the Encore Gigamax cache consistency protocols ( and ), In International Symposium on Shared Memory Multiprocessors, . [bibtex] [pdf]
[10] Analysis of digital circuits through symbolic reduction (), In IEEE Trans. on CAD of Integrated Circuits and Systems, volume 10, . [bibtex] [pdf] [doi]
[9] Synthesizing Converters Between Finite State Protocols (), In Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, ICCD '91, Cambridge, MA, USA, October 14-16, 1991, . [bibtex] [pdf] [doi]
[8] A language for compositional specification and verification of finite state hardware controllers (, and ), In Proceedings of the IEEE, volume 79, . [bibtex] [pdf]
1990
[7] Symbolic Model Checking: 10\^20 States and Beyond (), In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, . [bibtex] [pdf] [doi]
[6] Sequential Circuit Verification Using Symbolic Model Checking (), In Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, Florida, USA, June 24-28, 1990., . [bibtex] [pdf] [doi]
1989
[5] A Structural Induction Theorem for Processes (), In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing, Edmonton, Alberta, Canada, August 14-16, 1989, . [bibtex] [pdf] [doi]
[4] Compositional Model Checking (), In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, . [bibtex] [pdf] [doi]
[3] A language for compositional specification and verification of finite state hardware controllers (, and ), In CHDL 1989, . [bibtex] [pdf]
1986
[2]Software modules for a hand-scanned reading aid for the blind (, , , and ), In Proceedings of the Ninth Annual Conference on Rehabilitation Technology, . [bibtex]
[1]A Smart Trigger for real-time spike classification ( and ), In Proceedings of the Eighth Annual Conference of the IEEE/Engineering in Medicine and Biology Society, volume 1, . [bibtex]
Powered by bibtexbrowser