Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Kenneth L. McMillan
@article{DBLP:journals/pacmpl/TamirTMSHGS23,
author = {Orr Tamir and
Marcelo Taube and
Kenneth L. McMillan and
Sharon Shoham and
Jon Howell and
Guy Gueta and
Mooly Sagiv},
title = {Counterexample Driven Quantifier Instantiations with Applications
to Distributed Protocols},
journal = {Proc. {ACM} Program. Lang.},
volume = {7},
number = {{OOPSLA2}},
pages = {1878--1904},
year = {2023},
url = {https://doi.org/10.1145/3622864},
doi = {10.1145/3622864},
timestamp = {Sun, 10 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/TamirTMSHGS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kbse/HuWKMT23,
author = {Yang Hu and
Wenxi Wang and
Sarfraz Khurshid and
Kenneth L. McMillan and
Mohit Tiwari},
title = {Fixing Privilege Escalations in Cloud Access Control with MaxSAT and
Graph Neural Networks},
booktitle = {38th {IEEE/ACM} International Conference on Automated Software Engineering,
{ASE} 2023, Luxembourg, September 11-15, 2023},
pages = {104--115},
publisher = {{IEEE}},
year = {2023},
url = {https://doi.org/10.1109/ASE56229.2023.00167},
doi = {10.1109/ASE56229.2023.00167},
timestamp = {Thu, 16 Nov 2023 09:03:51 +0100},
biburl = {https://dblp.org/rec/conf/kbse/HuWKMT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/netys/HippelMNZ23,
author = {Max von Hippel and
Kenneth L. McMillan and
Cristina Nita{-}Rotaru and
Lenore D. Zuck},
editor = {David Mohaisen and
Thomas Wies},
title = {A Formal Analysis of Karn's Algorithm},
booktitle = {Networked Systems - 11th International Conference, {NETYS} 2023, Benguerir,
Morocco, May 22-24, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14067},
pages = {43--61},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-37765-5\_4},
doi = {10.1007/978-3-031-37765-5\_4},
timestamp = {Thu, 13 Jul 2023 14:30:34 +0200},
biburl = {https://dblp.org/rec/conf/netys/HippelMNZ23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/VickM23,
author = {Cole Vick and
Kenneth L. McMillan},
editor = {Cezara Dragoi and
Michael Emmi and
Jingbo Wang},
title = {Synthesizing History and Prophecy Variables for Symbolic Model Checking},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 24th International
Conference, {VMCAI} 2023, Boston, MA, USA, January 16-17, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13881},
pages = {320--340},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-24950-1\_15},
doi = {10.1007/978-3-031-24950-1\_15},
timestamp = {Mon, 30 Jan 2023 14:59:54 +0100},
biburl = {https://dblp.org/rec/conf/vmcai/VickM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08855,
author = {Max von Hippel and
Panagiotis Manolios and
Kenneth L. McMillan and
Cristina Nita{-}Rotaru and
Lenore D. Zuck},
editor = {Alessandro Coglio and
Sol Swords},
title = {A Case Study in Analytic Protocol Analysis in {ACL2}},
booktitle = {Proceedings of the 18th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, TX, {USA} and online, November
13-14, 2023},
series = {{EPTCS}},
volume = {393},
pages = {50--66},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.6},
doi = {10.4204/EPTCS.393.6},
timestamp = {Fri, 22 Dec 2023 11:34:10 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08855.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/PadonWKMA22,
author = {Oded Padon and
James R. Wilcox and
Jason R. Koenig and
Kenneth L. McMillan and
Alex Aiken},
title = {Induction duality: primal-dual search for invariants},
journal = {Proc. {ACM} Program. Lang.},
volume = {6},
number = {{POPL}},
pages = {1--29},
year = {2022},
url = {https://doi.org/10.1145/3498712},
doi = {10.1145/3498712},
timestamp = {Mon, 14 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/PadonWKMA22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sigsoft/WangHMK22,
author = {Wenxi Wang and
Yang Hu and
Kenneth L. McMillan and
Sarfraz Khurshid},
editor = {Abhik Roychoudhury and
Cristian Cadar and
Miryung Kim},
title = {SymMC: approximate model enumeration and counting using symmetry information
for Alloy specifications},
booktitle = {Proceedings of the 30th {ACM} Joint European Software Engineering
Conference and Symposium on the Foundations of Software Engineering,
{ESEC/FSE} 2022, Singapore, Singapore, November 14-18, 2022},
pages = {1209--1220},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3540250.3549161},
doi = {10.1145/3540250.3549161},
timestamp = {Thu, 10 Nov 2022 11:14:54 +0100},
biburl = {https://dblp.org/rec/conf/sigsoft/WangHMK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/PadonHMPSS21,
author = {Oded Padon and
Jochen Hoenicke and
Kenneth L. McMillan and
Andreas Podelski and
Mooly Sagiv and
Sharon Shoham},
title = {Temporal prophecy for proving temporal properties of infinite-state
systems},
journal = {Formal Methods Syst. Des.},
volume = {57},
number = {2},
pages = {246--269},
year = {2021},
url = {https://doi.org/10.1007/s10703-021-00377-1},
doi = {10.1007/S10703-021-00377-1},
timestamp = {Fri, 12 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/PadonHMPSS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2106-00966,
author = {Oded Padon and
Jochen Hoenicke and
Kenneth L. McMillan and
Andreas Podelski and
Mooly Sagiv and
Sharon Shoham},
title = {Temporal Prophecy for Proving Temporal Properties of Infinite-State
Systems},
journal = {CoRR},
volume = {abs/2106.00966},
year = {2021},
url = {https://arxiv.org/abs/2106.00966},
eprinttype = {arXiv},
eprint = {2106.00966},
timestamp = {Wed, 09 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2106-00966.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2110-14053,
author = {Wenxi Wang and
Yang Hu and
Mohit Tiwari and
Sarfraz Khurshid and
Kenneth L. McMillan and
Risto Miikkulainen},
title = {NeuroComb: Improving {SAT} Solving with Graph Neural Networks},
journal = {CoRR},
volume = {abs/2110.14053},
year = {2021},
url = {https://arxiv.org/abs/2110.14053},
eprinttype = {arXiv},
eprint = {2110.14053},
timestamp = {Fri, 12 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2110-14053.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillanP20,
author = {Kenneth L. McMillan and
Oded Padon},
editor = {Shuvendu K. Lahiri and
Chao Wang},
title = {Ivy: {A} Multi-modal Verification Tool for Distributed Algorithms},
booktitle = {Computer Aided Verification - 32nd International Conference, {CAV}
2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12225},
pages = {190--202},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-53291-8\_12},
doi = {10.1007/978-3-030-53291-8\_12},
timestamp = {Wed, 12 Aug 2020 15:15:44 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillanP20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2004-04198,
author = {Kenneth L. McMillan},
title = {Bayesian Interpolants as Explanations for Neural Inferences},
journal = {CoRR},
volume = {abs/2004.04198},
year = {2020},
url = {https://arxiv.org/abs/2004.04198},
eprinttype = {arXiv},
eprint = {2004.04198},
timestamp = {Tue, 14 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2004-04198.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/ZuckM19,
author = {Lenore D. Zuck and
Kenneth L. McMillan},
editor = {Ezio Bartocci and
Rance Cleaveland and
Radu Grosu and
Oleg Sokolsky},
title = {Invisible Invariants Are Neither},
booktitle = {From Reactive Systems to Cyber-Physical Systems - Essays Dedicated
to Scott A. Smolka on the Occasion of His 65th Birthday},
series = {Lecture Notes in Computer Science},
volume = {11500},
pages = {57--72},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-31514-6\_5},
doi = {10.1007/978-3-030-31514-6\_5},
timestamp = {Tue, 24 Sep 2019 14:08:41 +0200},
biburl = {https://dblp.org/rec/conf/birthday/ZuckM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/secdev/McMillanZ19,
author = {Kenneth L. McMillan and
Lenore D. Zuck},
title = {Compositional Testing of Internet Protocols},
booktitle = {2019 {IEEE} Cybersecurity Development, SecDev 2019, Tysons Corner,
VA, USA, September 23-25, 2019},
pages = {161--174},
publisher = {{IEEE}},
year = {2019},
url = {https://doi.org/10.1109/SecDev.2019.00031},
doi = {10.1109/SECDEV.2019.00031},
timestamp = {Wed, 27 Nov 2019 18:04:04 +0100},
biburl = {https://dblp.org/rec/conf/secdev/McMillanZ19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sigcomm/McMillanZ19,
author = {Kenneth L. McMillan and
Lenore D. Zuck},
editor = {Jianping Wu and
Wendy Hall},
title = {Formal specification and testing of {QUIC}},
booktitle = {Proceedings of the {ACM} Special Interest Group on Data Communication,
{SIGCOMM} 2019, Beijing, China, August 19-23, 2019},
pages = {227--240},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3341302.3342087},
doi = {10.1145/3341302.3342087},
timestamp = {Tue, 30 Nov 2021 14:57:49 +0100},
biburl = {https://dblp.org/rec/conf/sigcomm/McMillanZ19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan18,
author = {Kenneth L. McMillan},
editor = {Hana Chockler and
Georg Weissenbacher},
title = {Eager Abstraction for Symbolic Model Checking},
booktitle = {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}},
series = {Lecture Notes in Computer Science},
volume = {10981},
pages = {191--208},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96145-3\_11},
doi = {10.1007/978-3-319-96145-3\_11},
timestamp = {Fri, 09 Apr 2021 18:35:27 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/WangADM18,
author = {Xinyu Wang and
Greg Anderson and
Isil Dillig and
Kenneth L. McMillan},
editor = {Hana Chockler and
Georg Weissenbacher},
title = {Learning Abstractions for Program Synthesis},
booktitle = {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}},
series = {Lecture Notes in Computer Science},
volume = {10981},
pages = {407--426},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96145-3\_22},
doi = {10.1007/978-3-319-96145-3\_22},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/WangADM18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/PadonHMPSS18,
author = {Oded Padon and
Jochen Hoenicke and
Kenneth L. McMillan and
Andreas Podelski and
Mooly Sagiv and
Sharon Shoham},
editor = {Nikolaj S. Bj{\o}rner and
Arie Gurfinkel},
title = {Temporal Prophecy for Proving Temporal Properties of Infinite-State
Systems},
booktitle = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin,
TX, USA, October 30 - November 2, 2018},
pages = {1--11},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.23919/FMCAD.2018.8603008},
doi = {10.23919/FMCAD.2018.8603008},
timestamp = {Thu, 14 Apr 2022 20:26:15 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/PadonHMPSS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/TaubeLMPSSWW18,
author = {Marcelo Taube and
Giuliano Losa and
Kenneth L. McMillan and
Oded Padon and
Mooly Sagiv and
Sharon Shoham and
James R. Wilcox and
Doug Woos},
editor = {Jeffrey S. Foster and
Dan Grossman},
title = {Modularity for decidability of deductive verification with applications
to distributed systems},
booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2018, Philadelphia, PA,
USA, June 18-22, 2018},
pages = {662--677},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3192366.3192414},
doi = {10.1145/3192366.3192414},
timestamp = {Wed, 23 Jun 2021 15:34:31 +0200},
biburl = {https://dblp.org/rec/conf/pldi/TaubeLMPSSWW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/McMillanP18,
author = {Kenneth L. McMillan and
Oded Padon},
editor = {Andreas Podelski},
title = {Deductive Verification in Decidable Fragments with Ivy},
booktitle = {Static Analysis - 25th International Symposium, {SAS} 2018, Freiburg,
Germany, August 29-31, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11002},
pages = {43--55},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-99725-4\_4},
doi = {10.1007/978-3-319-99725-4\_4},
timestamp = {Mon, 28 Aug 2023 21:17:53 +0200},
biburl = {https://dblp.org/rec/conf/sas/McMillanP18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/ZuckMT18,
author = {Lenore D. Zuck and
Kenneth L. McMillan and
Jordan Torf},
editor = {Isil Dillig and
Jens Palsberg},
title = {P{\^{}}5 : Planner-less Proofs of Probabilistic Parameterized Protocols},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 19th International
Conference, {VMCAI} 2018, Los Angeles, CA, USA, January 7-9, 2018,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10747},
pages = {336--357},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-73721-8\_16},
doi = {10.1007/978-3-319-73721-8\_16},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/vmcai/ZuckMT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:reference/mc/McMillan18,
author = {Kenneth L. McMillan},
editor = {Edmund M. Clarke and
Thomas A. Henzinger and
Helmut Veith and
Roderick Bloem},
title = {Interpolation and Model Checking},
booktitle = {Handbook of Model Checking},
pages = {421--446},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-10575-8\_14},
doi = {10.1007/978-3-319-10575-8\_14},
timestamp = {Mon, 03 Jan 2022 22:13:30 +0100},
biburl = {https://dblp.org/rec/reference/mc/McMillan18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1804-04152,
author = {Xinyu Wang and
Greg Anderson and
Isil Dillig and
Kenneth L. McMillan},
title = {Learning Abstractions for Program Synthesis},
journal = {CoRR},
volume = {abs/1804.04152},
year = {2018},
url = {http://arxiv.org/abs/1804.04152},
eprinttype = {arXiv},
eprint = {1804.04152},
timestamp = {Wed, 19 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1804-04152.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sttt/DilligDLMS17,
author = {Isil Dillig and
Thomas Dillig and
Boyang Li and
Kenneth L. McMillan and
Mooly Sagiv},
title = {Synthesis of circular compositional program proofs via abduction},
journal = {Int. J. Softw. Tools Technol. Transf.},
volume = {19},
number = {5},
pages = {535--547},
year = {2017},
url = {https://doi.org/10.1007/s10009-015-0397-7},
doi = {10.1007/S10009-015-0397-7},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sttt/DilligDLMS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/McMillan16,
author = {Kenneth L. McMillan},
editor = {Ruzica Piskac and
Muralidhar Talupur},
title = {Modular specification and verification of a cache-coherent interface},
booktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain
View, CA, USA, October 3-6, 2016},
pages = {109--116},
publisher = {{IEEE}},
year = {2016},
url = {https://doi.org/10.1109/FMCAD.2016.7886668},
doi = {10.1109/FMCAD.2016.7886668},
timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/McMillan16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/PadonMPSS16,
author = {Oded Padon and
Kenneth L. McMillan and
Aurojit Panda and
Mooly Sagiv and
Sharon Shoham},
editor = {Chandra Krintz and
Emery D. Berger},
title = {Ivy: safety verification by interactive generalization},
booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2016, Santa Barbara, CA,
USA, June 13-17, 2016},
pages = {614--630},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2908080.2908118},
doi = {10.1145/2908080.2908118},
timestamp = {Sat, 30 Sep 2023 09:54:48 +0200},
biburl = {https://dblp.org/rec/conf/pldi/PadonMPSS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/BjornerGMR15,
author = {Nikolaj S. Bj{\o}rner and
Arie Gurfinkel and
Kenneth L. McMillan and
Andrey Rybalchenko},
editor = {Lev D. Beklemishev and
Andreas Blass and
Nachum Dershowitz and
Bernd Finkbeiner and
Wolfram Schulte},
title = {Horn Clause Solvers for Program Verification},
booktitle = {Fields of Logic and Computation {II} - Essays Dedicated to Yuri Gurevich
on the Occasion of His 75th Birthday},
series = {Lecture Notes in Computer Science},
volume = {9300},
pages = {24--51},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-23534-9\_2},
doi = {10.1007/978-3-319-23534-9\_2},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/birthday/BjornerGMR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/KomuravelliBGM15,
author = {Anvesh Komuravelli and
Nikolaj S. Bj{\o}rner and
Arie Gurfinkel and
Kenneth L. McMillan},
editor = {Roope Kaivola and
Thomas Wahl},
title = {Compositional Verification of Procedural Programs using Horn Clauses
over Integers and Arrays},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2015, Austin, Texas,
USA, September 27-30, 2015},
pages = {89--96},
publisher = {{IEEE}},
year = {2015},
url = {https://doi.org/10.1109/FMCAD.2015.7542257},
doi = {10.1109/FMCAD.2015.7542257},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/KomuravelliBGM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/KomuravelliBGM15,
author = {Anvesh Komuravelli and
Nikolaj S. Bj{\o}rner and
Arie Gurfinkel and
Kenneth L. McMillan},
title = {Compositional Verification of Procedural Programs using Horn Clauses
over Integers and Arrays},
journal = {CoRR},
volume = {abs/1508.01288},
year = {2015},
url = {http://arxiv.org/abs/1508.01288},
eprinttype = {arXiv},
eprint = {1508.01288},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KomuravelliBGM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigplan/HenzingerJMM14,
author = {Thomas A. Henzinger and
Ranjit Jhala and
Rupak Majumdar and
Kenneth L. McMillan},
title = {Abstractions from proofs},
journal = {{ACM} {SIGPLAN} Notices},
volume = {49},
number = {4S},
pages = {79--91},
year = {2014},
url = {https://doi.org/10.1145/2641638.2641655},
doi = {10.1145/2641638.2641655},
timestamp = {Wed, 11 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sigplan/HenzingerJMM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan14,
author = {Kenneth L. McMillan},
editor = {Armin Biere and
Roderick Bloem},
title = {Lazy Annotation Revisited},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {243--259},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08867-9\_16},
doi = {10.1007/978-3-319-08867-9\_16},
timestamp = {Mon, 03 Jan 2022 22:13:44 +0100},
biburl = {https://dblp.org/rec/conf/cav/McMillan14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/etaps/ZuckM14,
author = {Lenore D. Zuck and
Kenneth L. McMillan},
editor = {Saddek Bensalem and
Yassine Lakhnech and
Axel Legay},
title = {Reasoning about Network Topologies in Space},
booktitle = {From Programs to Systems. The Systems perspective in Computing - {ETAPS}
Workshop, {FPS} 2014, in Honor of Joseph Sifakis, Grenoble, France,
April 6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8415},
pages = {267--277},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-642-54848-2\_18},
doi = {10.1007/978-3-642-54848-2\_18},
timestamp = {Tue, 14 May 2019 10:00:36 +0200},
biburl = {https://dblp.org/rec/conf/etaps/ZuckM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2013s,
editor = {Kenneth L. McMillan and
Aart Middeldorp and
Geoff Sutcliffe and
Andrei Voronkov},
title = {{LPAR} 2013, 19th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch,
South Africa, Short papers proceedings},
series = {EPiC Series in Computing},
volume = {26},
publisher = {EasyChair},
year = {2014},
url = {https://easychair.org/publications/volume/LPAR-19},
timestamp = {Wed, 10 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lpar/2013s.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/vmcai/2014,
editor = {Kenneth L. McMillan and
Xavier Rival},
title = {Verification, Model Checking, and Abstract Interpretation - 15th International
Conference, {VMCAI} 2014, San Diego, CA, USA, January 19-21, 2014,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8318},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-642-54013-4},
doi = {10.1007/978-3-642-54013-4},
isbn = {978-3-642-54012-7},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/vmcai/2014.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/AlbarghouthiM13,
author = {Aws Albarghouthi and
Kenneth L. McMillan},
editor = {Natasha Sharygina and
Helmut Veith},
title = {Beautiful Interpolants},
booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8044},
pages = {313--329},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39799-8\_22},
doi = {10.1007/978-3-642-39799-8\_22},
timestamp = {Wed, 07 Dec 2022 23:12:58 +0100},
biburl = {https://dblp.org/rec/conf/cav/AlbarghouthiM13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/oopsla/DilligDLM13,
author = {Isil Dillig and
Thomas Dillig and
Boyang Li and
Kenneth L. McMillan},
editor = {Antony L. Hosking and
Patrick Th. Eugster and
Cristina V. Lopes},
title = {Inductive invariant generation via abductive inference},
booktitle = {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},
pages = {443--456},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2509136.2509511},
doi = {10.1145/2509136.2509511},
timestamp = {Sun, 27 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/oopsla/DilligDLM13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/BjornerMR13,
author = {Nikolaj S. Bj{\o}rner and
Kenneth L. McMillan and
Andrey Rybalchenko},
editor = {Francesco Logozzo and
Manuel F{\"{a}}hndrich},
title = {On Solving Universally Quantified Horn Clauses},
booktitle = {Static Analysis - 20th International Symposium, {SAS} 2013, Seattle,
WA, USA, June 20-22, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7935},
pages = {105--125},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-38856-9\_8},
doi = {10.1007/978-3-642-38856-9\_8},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sas/BjornerMR13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sbmf/McMillan13,
author = {Kenneth L. McMillan},
editor = {Juliano Iyoda and
Leonardo Mendon{\c{c}}a de Moura},
title = {Deductive Generalization},
booktitle = {Formal Methods: Foundations and Applications - 16th Brazilian Symposium,
{SBMF} 2013, Brasilia, Brazil, September 29 - October 4, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8195},
pages = {17},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-41071-0\_2},
doi = {10.1007/978-3-642-41071-0\_2},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/sbmf/McMillan13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sigsoft/LahiriMSH13,
author = {Shuvendu K. Lahiri and
Kenneth L. McMillan and
Rahul Sharma and
Chris Hawblitzel},
editor = {Bertrand Meyer and
Luciano Baresi and
Mira Mezini},
title = {Differential assertion checking},
booktitle = {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},
pages = {345--355},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2491411.2491452},
doi = {10.1145/2491411.2491452},
timestamp = {Tue, 01 Feb 2022 10:45:16 +0100},
biburl = {https://dblp.org/rec/conf/sigsoft/LahiriMSH13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/LiDDMS13,
author = {Boyang Li and
Isil Dillig and
Thomas Dillig and
Kenneth L. McMillan and
Mooly Sagiv},
editor = {Nir Piterman and
Scott A. Smolka},
title = {Synthesis of Circular Compositional Program Proofs via Abduction},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {7795},
pages = {370--384},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-36742-7\_26},
doi = {10.1007/978-3-642-36742-7\_26},
timestamp = {Sun, 27 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/LiDDMS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2013,
editor = {Kenneth L. McMillan and
Aart Middeldorp and
Andrei Voronkov},
title = {Logic for Programming, Artificial Intelligence, and Reasoning - 19th
International Conference, LPAR-19, Stellenbosch, South Africa, December
14-19, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8312},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-45221-5},
doi = {10.1007/978-3-642-45221-5},
isbn = {978-3-642-45220-8},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2013.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BjornerMR13,
author = {Nikolaj S. Bj{\o}rner and
Kenneth L. McMillan and
Andrey Rybalchenko},
title = {Higher-order Program Verification as Satisfiability Modulo Theories
with Algebraic Data-types},
journal = {CoRR},
volume = {abs/1306.5264},
year = {2013},
url = {http://arxiv.org/abs/1306.5264},
eprinttype = {arXiv},
eprint = {1306.5264},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BjornerMR13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BjornerMR12,
author = {Nikolaj S. Bj{\o}rner and
Kenneth L. McMillan and
Andrey Rybalchenko},
editor = {Pascal Fontaine and
Amit Goel},
title = {Program Verification as Satisfiability Modulo Theories},
booktitle = {10th International Workshop on Satisfiability Modulo Theories, {SMT}
2012, Manchester, UK, June 30 - July 1, 2012},
series = {EPiC Series in Computing},
volume = {20},
pages = {3--11},
publisher = {EasyChair},
year = {2012},
url = {https://doi.org/10.29007/1l7f},
doi = {10.29007/1L7F},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BjornerMR12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/DilligDMA12,
author = {Isil Dillig and
Thomas Dillig and
Kenneth L. McMillan and
Alex Aiken},
editor = {P. Madhusudan and
Sanjit A. Seshia},
title = {Minimum Satisfying Assignments for {SMT}},
booktitle = {Computer Aided Verification - 24th International Conference, {CAV}
2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7358},
pages = {394--409},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31424-7\_30},
doi = {10.1007/978-3-642-31424-7\_30},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/DilligDMA12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/spin/BallBMMV12,
author = {Thomas Ball and
Nikolaj S. Bj{\o}rner and
Leonardo Mendon{\c{c}}a de Moura and
Kenneth L. McMillan and
Margus Veanes},
editor = {Alastair F. Donaldson and
David Parker},
title = {Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata
and Polynomials},
booktitle = {Model Checking Software - 19th International Workshop, {SPIN} 2012,
Oxford, UK, July 23-24, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7385},
pages = {1--6},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31759-0\_1},
doi = {10.1007/978-3-642-31759-0\_1},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/spin/BallBMMV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/McMillan11,
author = {Kenneth L. McMillan},
editor = {Per Bjesse and
Anna Slobodov{\'{a}}},
title = {Interpolants from {Z3} proofs},
booktitle = {International Conference on Formal Methods in Computer-Aided Design,
{FMCAD} '11, Austin, TX, USA, October 30 - November 02, 2011},
pages = {19--27},
publisher = {{FMCAD} Inc.},
year = {2011},
url = {http://dl.acm.org/citation.cfm?id=2157661},
timestamp = {Mon, 09 Aug 2021 15:21:44 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/McMillan11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/McMillan11,
author = {Kenneth L. McMillan},
editor = {Eran Yahav},
title = {Widening and Interpolation},
booktitle = {Static Analysis - 18th International Symposium, {SAS} 2011, Venice,
Italy, September 14-16, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6887},
pages = {1},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-23702-7\_1},
doi = {10.1007/978-3-642-23702-7\_1},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/sas/McMillan11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/McMillanZ11,
author = {Kenneth L. McMillan and
Lenore D. Zuck},
editor = {Eran Yahav},
title = {Invisible Invariants and Abstract Interpretation},
booktitle = {Static Analysis - 18th International Symposium, {SAS} 2011, Venice,
Italy, September 14-16, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6887},
pages = {249--262},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-23702-7\_20},
doi = {10.1007/978-3-642-23702-7\_20},
timestamp = {Wed, 24 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sas/McMillanZ11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan10,
author = {Kenneth L. McMillan},
editor = {Tayssir Touili and
Byron Cook and
Paul B. Jackson},
title = {Lazy Annotation for Program Testing and Verification},
booktitle = {Computer Aided Verification, 22nd International Conference, {CAV}
2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6174},
pages = {104--118},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14295-6\_10},
doi = {10.1007/978-3-642-14295-6\_10},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillanKS09,
author = {Kenneth L. McMillan and
Andreas Kuehlmann and
Mooly Sagiv},
editor = {Ahmed Bouajjani and
Oded Maler},
title = {Generalizing {DPLL} to Richer Logics},
booktitle = {Computer Aided Verification, 21st International Conference, {CAV}
2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5643},
pages = {462--476},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02658-4\_35},
doi = {10.1007/978-3-642-02658-4\_35},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillanKS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmics/McMillan09,
author = {Kenneth L. McMillan},
editor = {Mar{\'{\i}}a Alpuente and
Byron Cook and
Christophe Joubert},
title = {What's in Common between Test, Model Checking, and Decision Procedures?},
booktitle = {Formal Methods for Industrial Critical Systems, 14th International
Workshop, {FMICS} 2009, Eindhoven, The Netherlands, November 2-3,
2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5825},
pages = {35--36},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04570-7\_4},
doi = {10.1007/978-3-642-04570-7\_4},
timestamp = {Sun, 02 Oct 2022 16:01:27 +0200},
biburl = {https://dblp.org/rec/conf/fmics/McMillan09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rp/McMillanZ09,
author = {Kenneth L. McMillan and
Lenore D. Zuck},
editor = {Olivier Bournez and
Igor Potapov},
title = {Abstract Counterexamples for Non-disjunctive Abstractions},
booktitle = {Reachability Problems, 3rd International Workshop, {RP} 2009, Palaiseau,
France, September 23-25, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5797},
pages = {176--188},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04420-5\_17},
doi = {10.1007/978-3-642-04420-5\_17},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/rp/McMillanZ09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/GuptaMF08,
author = {Anubhav Gupta and
Kenneth L. McMillan and
Zhaohui Fu},
title = {Automated assumption generation for compositional verification},
journal = {Formal Methods Syst. Des.},
volume = {32},
number = {3},
pages = {285--301},
year = {2008},
url = {https://doi.org/10.1007/s10703-008-0050-0},
doi = {10.1007/S10703-008-0050-0},
timestamp = {Fri, 01 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/GuptaMF08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hvc/McMillan08,
author = {Kenneth L. McMillan},
editor = {Hana Chockler and
Alan J. Hu},
title = {Proofs, Interpolants, and Relevance Heuristics},
booktitle = {Hardware and Software: Verification and Testing, 4th International
Haifa Verification Conference, {HVC} 2008, Haifa, Israel, October
27-30, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5394},
pages = {3},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-01702-5\_3},
doi = {10.1007/978-3-642-01702-5\_3},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/hvc/McMillan08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/McMillan08,
author = {Kenneth L. McMillan},
editor = {George C. Necula and
Philip Wadler},
title = {Relevance heuristics for program analysis},
booktitle = {Proceedings of the 35th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2008, San Francisco, California,
USA, January 7-12, 2008},
pages = {145--146},
publisher = {{ACM}},
year = {2008},
url = {https://doi.org/10.1145/1328438.1328440},
doi = {10.1145/1328438.1328440},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/popl/McMillan08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/McMillan08,
author = {Kenneth L. McMillan},
editor = {C. R. Ramakrishnan and
Jakob Rehof},
title = {Quantified Invariant Generation Using an Interpolating Saturation
Prover},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {4963},
pages = {413--427},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-78800-3\_31},
doi = {10.1007/978-3-540-78800-3\_31},
timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
biburl = {https://dblp.org/rec/conf/tacas/McMillan08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/JhalaM07,
author = {Ranjit Jhala and
Kenneth L. McMillan},
title = {Interpolant-Based Transition Relation Approximation},
journal = {Log. Methods Comput. Sci.},
volume = {3},
number = {4},
year = {2007},
url = {https://doi.org/10.2168/LMCS-3(4:1)2007},
doi = {10.2168/LMCS-3(4:1)2007},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/JhalaM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/atva/McMillan07,
author = {Kenneth L. McMillan},
editor = {Kedar S. Namjoshi and
Tomohiro Yoneda and
Teruo Higashino and
Yoshio Okamura},
title = {Toward Property-Driven Abstraction for Heap Manipulating Programs},
booktitle = {Automated Technology for Verification and Analysis, 5th International
Symposium, {ATVA} 2007, Tokyo, Japan, October 22-25, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4762},
pages = {17--18},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-75596-8\_3},
doi = {10.1007/978-3-540-75596-8\_3},
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
biburl = {https://dblp.org/rec/conf/atva/McMillan07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/JhalaM07,
author = {Ranjit Jhala and
Kenneth L. McMillan},
editor = {Werner Damm and
Holger Hermanns},
title = {Array Abstractions from Proofs},
booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
2007, Berlin, Germany, July 3-7, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4590},
pages = {193--206},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73368-3\_23},
doi = {10.1007/978-3-540-73368-3\_23},
timestamp = {Sat, 30 Sep 2023 09:35:55 +0200},
biburl = {https://dblp.org/rec/conf/cav/JhalaM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/GuptaMF07,
author = {Anubhav Gupta and
Kenneth L. McMillan and
Zhaohui Fu},
editor = {Werner Damm and
Holger Hermanns},
title = {Automated Assumption Generation for Compositional Verification},
booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
2007, Berlin, Germany, July 3-7, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4590},
pages = {420--432},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73368-3\_45},
doi = {10.1007/978-3-540-73368-3\_45},
timestamp = {Fri, 01 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cav/GuptaMF07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/AmlaM07,
author = {Nina Amla and
Kenneth L. McMillan},
editor = {Orna Grumberg and
Michael Huth},
title = {Combining Abstraction Refinement and SAT-Based Model Checking},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {4424},
pages = {405--419},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-71209-1\_31},
doi = {10.1007/978-3-540-71209-1\_31},
timestamp = {Mon, 11 Sep 2023 15:43:49 +0200},
biburl = {https://dblp.org/rec/conf/tacas/AmlaM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/McMillan07,
author = {Kenneth L. McMillan},
editor = {Byron Cook and
Andreas Podelski},
title = {Interpolants and Symbolic Model Checking},
booktitle = {Verification, Model Checking, and Abstract Interpretation, 8th International
Conference, {VMCAI} 2007, Nice, France, January 14-16, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4349},
pages = {89--90},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-69738-1\_6},
doi = {10.1007/978-3-540-69738-1\_6},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/vmcai/McMillan07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0706-0523,
author = {Ranjit Jhala and
Kenneth L. McMillan},
title = {Interpolant-Based Transition Relation Approximation},
journal = {CoRR},
volume = {abs/0706.0523},
year = {2007},
url = {http://arxiv.org/abs/0706.0523},
eprinttype = {arXiv},
eprint = {0706.0523},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0706-0523.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan06,
author = {Kenneth L. McMillan},
editor = {Thomas Ball and
Robert B. Jones},
title = {Lazy Abstraction with Interpolants},
booktitle = {Computer Aided Verification, 18th International Conference, {CAV}
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4144},
pages = {123--136},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11817963\_14},
doi = {10.1007/11817963\_14},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/forte/FangMPZ06,
author = {Yi Fang and
Kenneth L. McMillan and
Amir Pnueli and
Lenore D. Zuck},
editor = {Elie Najm and
Jean{-}Fran{\c{c}}ois Pradat{-}Peyre and
V{\'{e}}ronique Donzeau{-}Gouge},
title = {Liveness by Invisible Invariants},
booktitle = {Formal Techniques for Networked and Distributed Systems - {FORTE}
2006, 26th {IFIP} {WG} 6.1 International Conference, Paris, France,
September 26-29, 2006},
series = {Lecture Notes in Computer Science},
volume = {4229},
pages = {356--371},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11888116\_26},
doi = {10.1007/11888116\_26},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/forte/FangMPZ06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/JhalaM06,
author = {Ranjit Jhala and
Kenneth L. McMillan},
editor = {Holger Hermanns and
Jens Palsberg},
title = {A Practical and Complete Approach to Predicate Refinement},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {3920},
pages = {459--473},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11691372\_33},
doi = {10.1007/11691372\_33},
timestamp = {Sat, 30 Sep 2023 09:57:43 +0200},
biburl = {https://dblp.org/rec/conf/tacas/JhalaM06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/AlurMP05,
author = {Rajeev Alur and
Kenneth L. McMillan and
Doron A. Peled},
title = {Deciding Global Partial-Order Properties},
journal = {Formal Methods Syst. Des.},
volume = {26},
number = {1},
pages = {7--25},
year = {2005},
url = {https://doi.org/10.1007/s10703-005-4592-0},
doi = {10.1007/S10703-005-4592-0},
timestamp = {Fri, 13 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/AlurMP05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/McMillan05,
author = {Kenneth L. McMillan},
title = {An interpolating theorem prover},
journal = {Theor. Comput. Sci.},
volume = {345},
number = {1},
pages = {101--121},
year = {2005},
url = {https://doi.org/10.1016/j.tcs.2005.07.003},
doi = {10.1016/J.TCS.2005.07.003},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/McMillan05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/apn/McMillan05,
author = {Kenneth L. McMillan},
editor = {Gianfranco Ciardo and
Philippe Darondeau},
title = {Applications of Craig Interpolation to Model Checking},
booktitle = {Applications and Theory of Petri Nets 2005, 26th International Conference,
{ICATPN} 2005, Miami, USA, June 20-25, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3536},
pages = {15--16},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11494744\_2},
doi = {10.1007/11494744\_2},
timestamp = {Tue, 14 May 2019 10:00:45 +0200},
biburl = {https://dblp.org/rec/conf/apn/McMillan05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/JhalaM05,
author = {Ranjit Jhala and
Kenneth L. McMillan},
editor = {Kousha Etessami and
Sriram K. Rajamani},
title = {Interpolant-Based Transition Relation Approximation},
booktitle = {Computer Aided Verification, 17th International Conference, {CAV}
2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3576},
pages = {39--51},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11513988\_6},
doi = {10.1007/11513988\_6},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/JhalaM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/charme/AmlaDKKM05,
author = {Nina Amla and
Xiaoqun Du and
Andreas Kuehlmann and
Robert P. Kurshan and
Kenneth L. McMillan},
editor = {Dominique Borrione and
Wolfgang J. Paul},
title = {An Analysis of SAT-Based Model Checking Techniques in an Industrial
Environment},
booktitle = {Correct Hardware Design and Verification Methods, 13th {IFIP} {WG}
10.5 Advanced Research Working Conference, {CHARME} 2005, Saarbr{\"{u}}cken,
Germany, October 3-6, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3725},
pages = {254--268},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11560548\_20},
doi = {10.1007/11560548\_20},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/charme/AmlaDKKM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/McMillan05,
author = {Kenneth L. McMillan},
editor = {Nicolas Halbwachs and
Lenore D. Zuck},
title = {Applications of Craig Interpolants in Model Checking},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {3440},
pages = {1--12},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/978-3-540-31980-1\_1},
doi = {10.1007/978-3-540-31980-1\_1},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/tacas/McMillan05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/McMillan04,
author = {Kenneth L. McMillan},
editor = {Jerzy Marcinkowski and
Andrzej Tarlecki},
title = {Applications of Craig Interpolation to Model Checking},
booktitle = {Computer Science Logic, 18th International Workshop, {CSL} 2004, 13th
Annual Conference of the EACSL, Karpacz, Poland, September 20-24,
2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3210},
pages = {22--23},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-30124-0\_3},
doi = {10.1007/978-3-540-30124-0\_3},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/McMillan04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/AmlaM04,
author = {Nina Amla and
Kenneth L. McMillan},
editor = {Alan J. Hu and
Andrew K. Martin},
title = {A Hybrid of Counterexample-Based and Proof-Based Abstraction},
booktitle = {Formal Methods in Computer-Aided Design, 5th International Conference,
{FMCAD} 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3312},
pages = {260--274},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-30494-4\_19},
doi = {10.1007/978-3-540-30494-4\_19},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/AmlaM04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/HenzingerJMM04,
author = {Thomas A. Henzinger and
Ranjit Jhala and
Rupak Majumdar and
Kenneth L. McMillan},
editor = {Neil D. Jones and
Xavier Leroy},
title = {Abstractions from proofs},
booktitle = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2004, Venice, Italy, January 14-16,
2004},
pages = {232--244},
publisher = {{ACM}},
year = {2004},
url = {https://doi.org/10.1145/964001.964021},
doi = {10.1145/964001.964021},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/popl/HenzingerJMM04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/McMillan04,
author = {Kenneth L. McMillan},
editor = {Kurt Jensen and
Andreas Podelski},
title = {An Interpolating Theorem Prover},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {2988},
pages = {16--30},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-24730-2\_2},
doi = {10.1007/978-3-540-24730-2\_2},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/tacas/McMillan04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan03,
author = {Kenneth L. McMillan},
editor = {Warren A. Hunt Jr. and
Fabio Somenzi},
title = {Interpolation and SAT-Based Model Checking},
booktitle = {Computer Aided Verification, 15th International Conference, {CAV}
2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2725},
pages = {1--13},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-45069-6\_1},
doi = {10.1007/978-3-540-45069-6\_1},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/memocode/McMillan03,
author = {Kenneth L. McMillan},
title = {Methods for exploiting {SAT} solvers in unbounded model checking},
booktitle = {1st {ACM} {\&} {IEEE} International Conference on Formal Methods
and Models for Co-Design {(MEMOCODE} 2003), 24-26 June 2003, Mont
Saint-Michel, France, Proceedings},
pages = {135},
publisher = {{IEEE} Computer Society},
year = {2003},
url = {https://doi.org/10.1109/MEMCOD.2003.1210098},
doi = {10.1109/MEMCOD.2003.1210098},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/memocode/McMillan03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/McMillan03,
author = {Kenneth L. McMillan},
editor = {Radhia Cousot},
title = {Craig Interpolation and Reachability Analysis},
booktitle = {Static Analysis, 10th International Symposium, {SAS} 2003, San Diego,
CA, USA, June 11-13, 2003, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2694},
pages = {336},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/3-540-44898-5\_18},
doi = {10.1007/3-540-44898-5\_18},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/sas/McMillan03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/McMillanA03,
author = {Kenneth L. McMillan and
Nina Amla},
editor = {Hubert Garavel and
John Hatcliff},
title = {Automatic Abstraction without Counterexamples},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {2--17},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/3-540-36577-X\_2},
doi = {10.1007/3-540-36577-X\_2},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/tacas/McMillanA03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/AmlaKMM03,
author = {Nina Amla and
Robert P. Kurshan and
Kenneth L. McMillan and
Ricardo H. Medel},
editor = {Hubert Garavel and
John Hatcliff},
title = {Experimental Analysis of Different Techniques for Bounded Model Checking},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {34--48},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/3-540-36577-X\_4},
doi = {10.1007/3-540-36577-X\_4},
timestamp = {Sat, 13 Apr 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/AmlaKMM03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan02,
author = {Kenneth L. McMillan},
editor = {Ed Brinksma and
Kim Guldstrand Larsen},
title = {Applying {SAT} Methods in Unbounded Symbolic Model Checking},
booktitle = {Computer Aided Verification, 14th International Conference, {CAV}
2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2404},
pages = {250--264},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45657-0\_19},
doi = {10.1007/3-540-45657-0\_19},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcad/CarloniMS01,
author = {Luca P. Carloni and
Kenneth L. McMillan and
Alberto L. Sangiovanni{-}Vincentelli},
title = {Theory of latency-insensitive design},
journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
volume = {20},
number = {9},
pages = {1059--1076},
year = {2001},
url = {https://doi.org/10.1109/43.945302},
doi = {10.1109/43.945302},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcad/CarloniMS01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/JhalaM01,
author = {Ranjit Jhala and
Kenneth L. McMillan},
editor = {G{\'{e}}rard Berry and
Hubert Comon and
Alain Finkel},
title = {Microarchitecture Verification by Compositional Model Checking},
booktitle = {Computer Aided Verification, 13th International Conference, {CAV}
2001, Paris, France, July 18-22, 2001, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2102},
pages = {396--410},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-44585-4\_40},
doi = {10.1007/3-540-44585-4\_40},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/JhalaM01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/charme/McMillan01,
author = {Kenneth L. McMillan},
editor = {Tiziana Margaria and
Thomas F. Melham},
title = {Parameterized Verification of the {FLASH} Cache Coherence Protocol
by Compositional Model Checking},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {2144},
pages = {179--195},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-44798-9\_17},
doi = {10.1007/3-540-44798-9\_17},
timestamp = {Sun, 02 Jun 2019 21:23:48 +0200},
biburl = {https://dblp.org/rec/conf/charme/McMillan01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/AlurMP00,
author = {Rajeev Alur and
Kenneth L. McMillan and
Doron A. Peled},
title = {Model-Checking of Correctness Conditions for Concurrent Objects},
journal = {Inf. Comput.},
volume = {160},
number = {1-2},
pages = {167--188},
year = {2000},
url = {https://doi.org/10.1006/inco.1999.2847},
doi = {10.1006/INCO.1999.2847},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/AlurMP00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/scp/McMillan00,
author = {Kenneth L. McMillan},
title = {A methodology for hardware verification using compositional model
checking},
journal = {Sci. Comput. Program.},
volume = {37},
number = {1-3},
pages = {279--309},
year = {2000},
url = {https://doi.org/10.1016/S0167-6423(99)00030-1},
doi = {10.1016/S0167-6423(99)00030-1},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/scp/McMillan00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcad/HongBBM00,
author = {Youpyo Hong and
Peter A. Beerel and
Jerry R. Burch and
Kenneth L. McMillan},
title = {Sibling-substitution-based {BDD} minimization using don't cares},
journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
volume = {19},
number = {1},
pages = {44--55},
year = {2000},
url = {https://doi.org/10.1109/43.822619},
doi = {10.1109/43.822619},
timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcad/HongBBM00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillanQS00,
author = {Kenneth L. McMillan and
Shaz Qadeer and
James B. Saxe},
editor = {E. Allen Emerson and
A. Prasad Sistla},
title = {Induction in Compositional Model Checking},
booktitle = {Computer Aided Verification, 12th International Conference, {CAV}
2000, Chicago, IL, USA, July 15-19, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1855},
pages = {312--327},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10722167\_25},
doi = {10.1007/10722167\_25},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillanQS00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/McMillan00,
author = {Kenneth L. McMillan},
title = {Some Strategies for Proving Theorems with a Model Checker},
booktitle = {15th Annual {IEEE} Symposium on Logic in Computer Science, Santa Barbara,
California, USA, June 26-29, 2000},
pages = {305--306},
publisher = {{IEEE} Computer Society},
year = {2000},
url = {https://doi.org/10.1109/LICS.2000.855778},
doi = {10.1109/LICS.2000.855778},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/McMillan00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CarloniMS99,
author = {Luca P. Carloni and
Kenneth L. McMillan and
Alberto L. Sangiovanni{-}Vincentelli},
editor = {Nicolas Halbwachs and
Doron A. Peled},
title = {Latency Insensitive Protocols},
booktitle = {Computer Aided Verification, 11th International Conference, {CAV}
'99, Trento, Italy, July 6-10, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1633},
pages = {123--133},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48683-6\_13},
doi = {10.1007/3-540-48683-6\_13},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/CarloniMS99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/charme/McMillan99,
author = {Kenneth L. McMillan},
editor = {Laurence Pierre and
Thomas Kropf},
title = {Verification of Infinite State Systems by Compositional Model Checking},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {1703},
pages = {219--234},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48153-2\_17},
doi = {10.1007/3-540-48153-2\_17},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/charme/McMillan99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/charme/McMillan99a,
author = {Kenneth L. McMillan},
editor = {Laurence Pierre and
Thomas Kropf},
title = {Circular Compositional Reasoning about Liveness},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {1703},
pages = {342--345},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48153-2\_30},
doi = {10.1007/3-540-48153-2\_30},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/charme/McMillan99a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccad/CarloniMSS99,
author = {Luca P. Carloni and
Kenneth L. McMillan and
Alexander Saldanha and
Alberto L. Sangiovanni{-}Vincentelli},
editor = {Jacob K. White and
Ellen Sentovich},
title = {A methodology for correct-by-construction latency insensitive design},
booktitle = {Proceedings of the 1999 {IEEE/ACM} International Conference on Computer-Aided
Design, 1999, San Jose, California, USA, November 7-11, 1999},
pages = {309--315},
publisher = {{IEEE} Computer Society},
year = {1999},
url = {https://doi.org/10.1109/ICCAD.1999.810667},
doi = {10.1109/ICCAD.1999.810667},
timestamp = {Mon, 08 May 2023 21:43:38 +0200},
biburl = {https://dblp.org/rec/conf/iccad/CarloniMSS99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccad/KuehlmannMB99,
author = {Andreas Kuehlmann and
Kenneth L. McMillan and
Robert K. Brayton},
editor = {Jacob K. White and
Ellen Sentovich},
title = {Probabilistic state space search},
booktitle = {Proceedings of the 1999 {IEEE/ACM} International Conference on Computer-Aided
Design, 1999, San Jose, California, USA, November 7-11, 1999},
pages = {574--579},
publisher = {{IEEE} Computer Society},
year = {1999},
url = {https://doi.org/10.1109/ICCAD.1999.810713},
doi = {10.1109/ICCAD.1999.810713},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/iccad/KuehlmannMB99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan98,
author = {Kenneth L. McMillan},
editor = {Alan J. Hu and
Moshe Y. Vardi},
title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional
Model Checking},
booktitle = {Computer Aided Verification, 10th International Conference, {CAV}
'98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1427},
pages = {110--121},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/BFb0028738},
doi = {10.1007/BFB0028738},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/RaviMSS98,
author = {Kavita Ravi and
Kenneth L. McMillan and
Thomas R. Shiple and
Fabio Somenzi},
editor = {Basant R. Chawla and
Randal E. Bryant and
Jan M. Rabaey},
title = {Approximation and Decomposition of Binary Decision Diagrams},
booktitle = {Proceedings of the 35th Conference on Design Automation, Moscone center,
San Francico, California, USA, June 15-19, 1998},
pages = {445--450},
publisher = {{ACM} Press},
year = {1998},
url = {https://doi.org/10.1145/277044.277168},
doi = {10.1145/277044.277168},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/RaviMSS98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/McMillan98,
author = {Kenneth L. McMillan},
editor = {Ganesh Gopalakrishnan and
Phillip J. Windley},
title = {Minimalist Proof Assistants: Interactions of Technology and Methodology
in Formal System Level Verification (abstract)},
booktitle = {Formal Methods in Computer-Aided Design, Second International Conference,
{FMCAD} '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1522},
pages = {1},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/3-540-49519-3\_1},
doi = {10.1007/3-540-49519-3\_1},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/McMillan98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fsttcs/McMillan98,
author = {Kenneth L. McMillan},
editor = {Vikraman Arvind and
Ramaswamy Ramanujam},
title = {Proof Rules for Model Checking Systems with Data},
booktitle = {Foundations of Software Technology and Theoretical Computer Science,
18th Conference, Chennai, India, December 17-19, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1530},
pages = {270},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/978-3-540-49382-2\_25},
doi = {10.1007/978-3-540-49382-2\_25},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/fsttcs/McMillan98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/AlurMP98,
author = {Rajeev Alur and
Kenneth L. McMillan and
Doron A. Peled},
editor = {Kim Guldstrand Larsen and
Sven Skyum and
Glynn Winskel},
title = {Deciding Global Partial-Order Properties},
booktitle = {Automata, Languages and Programming, 25th International Colloquium,
ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1443},
pages = {41--52},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/BFb0055039},
doi = {10.1007/BFB0055039},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/icalp/AlurMP98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/ClarkeMZFY97,
author = {Edmund M. Clarke and
Kenneth L. McMillan and
Xudong Zhao and
Masahiro Fujita and
Jerry Chih{-}Yuan Yang},
title = {Spectral Transforms for Large Boolean Functions with Applications
to Technology Mapping},
journal = {Formal Methods Syst. Des.},
volume = {10},
number = {2/3},
pages = {137--148},
year = {1997},
url = {https://doi.org/10.1023/A:1008695706493},
doi = {10.1023/A:1008695706493},
timestamp = {Tue, 17 Nov 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/ClarkeMZFY97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan97,
author = {Kenneth L. McMillan},
editor = {Orna Grumberg},
title = {A Compositional Rule for Hardware Design Refinement},
booktitle = {Computer Aided Verification, 9th International Conference, {CAV} '97,
Haifa, Israel, June 22-25, 1997, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1254},
pages = {24--35},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-63166-6\_6},
doi = {10.1007/3-540-63166-6\_6},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/HongBBM97,
author = {Youpyo Hong and
Peter A. Beerel and
Jerry R. Burch and
Kenneth L. McMillan},
editor = {Ellen J. Yoffa and
Giovanni De Micheli and
Jan M. Rabaey},
title = {Safe {BDD} Minimization Using Don't Cares},
booktitle = {Proceedings of the 34st Conference on Design Automation, Anaheim,
California, USA, Anaheim Convention Center, June 9-13, 1997},
pages = {208--213},
publisher = {{ACM} Press},
year = {1997},
url = {https://doi.org/10.1145/266021.266068},
doi = {10.1145/266021.266068},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/HongBBM97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan96,
author = {Kenneth L. McMillan},
editor = {Rajeev Alur and
Thomas A. Henzinger},
title = {A Conjunctively Decomposed Boolean Representation for Symbolic Model
Checking},
booktitle = {Computer Aided Verification, 8th International Conference, {CAV} '96,
New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1102},
pages = {13--25},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61474-5\_54},
doi = {10.1007/3-540-61474-5\_54},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ClarkeMCH96,
author = {Edmund M. Clarke and
Kenneth L. McMillan and
S{\'{e}}rgio Vale Aguiar Campos and
Vasiliki Hartonas{-}Garmhausen},
editor = {Rajeev Alur and
Thomas A. Henzinger},
title = {Symbolic Model Checking},
booktitle = {Computer Aided Verification, 8th International Conference, {CAV} '96,
New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1102},
pages = {419--427},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61474-5\_93},
doi = {10.1007/3-540-61474-5\_93},
timestamp = {Mon, 22 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/ClarkeMCH96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/KhatriNKMBS96,
author = {Sunil P. Khatri and
Amit Narayan and
Sriram C. Krishnan and
Kenneth L. McMillan and
Robert K. Brayton and
Alberto L. Sangiovanni{-}Vincentelli},
editor = {Thomas Pennino and
Ellen J. Yoffa},
title = {Engineering Change in a Non-Deterministic {FSM} Setting},
booktitle = {Proceedings of the 33st Conference on Design Automation, Las Vegas,
Nevada, USA, Las Vegas Convention Center, June 3-7, 1996},
pages = {451--456},
publisher = {{ACM} Press},
year = {1996},
url = {https://doi.org/10.1145/240518.240604},
doi = {10.1145/240518.240604},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/KhatriNKMBS96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/AlurMP96,
author = {Rajeev Alur and
Kenneth L. McMillan and
Doron A. Peled},
title = {Model-Checking of Correctness Conditions for Concurrent Objects},
booktitle = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
New Brunswick, New Jersey, USA, July 27-30, 1996},
pages = {219--228},
publisher = {{IEEE} Computer Society},
year = {1996},
url = {https://doi.org/10.1109/LICS.1996.561322},
doi = {10.1109/LICS.1996.561322},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/AlurMP96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/McMillan95,
author = {Kenneth L. McMillan},
title = {A Technique of State Space Search Based on Unfolding},
journal = {Formal Methods Syst. Des.},
volume = {6},
number = {1},
pages = {45--65},
year = {1995},
url = {https://doi.org/10.1007/BF01384314},
doi = {10.1007/BF01384314},
timestamp = {Fri, 13 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/McMillan95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/ClarkeGHJLMN95,
author = {Edmund M. Clarke and
Orna Grumberg and
Hiromi Hiraishi and
Somesh Jha and
David E. Long and
Kenneth L. McMillan and
Linda A. Ness},
title = {Verification of the Futurebus+ Cache Coherence Protocol},
journal = {Formal Methods Syst. Des.},
volume = {6},
number = {2},
pages = {217--232},
year = {1995},
url = {https://doi.org/10.1007/BF01383968},
doi = {10.1007/BF01383968},
timestamp = {Fri, 13 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/ClarkeGHJLMN95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/KurshanM95,
author = {Robert P. Kurshan and
Kenneth L. McMillan},
title = {A Structural Induction Theorem for Processes},
journal = {Inf. Comput.},
volume = {117},
number = {1},
pages = {1--11},
year = {1995},
url = {https://doi.org/10.1006/inco.1995.1024},
doi = {10.1006/INCO.1995.1024},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/KurshanM95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan95,
author = {Kenneth L. McMillan},
editor = {Pierre Wolper},
title = {Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings},
booktitle = {Computer Aided Verification, 7th International Conference, Li{\`{e}}ge,
Belgium, July, 3-5, 1995, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {939},
pages = {180--195},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-60045-0\_50},
doi = {10.1007/3-540-60045-0\_50},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/EirikssonM95,
author = {{\'{A}}sgeir Th. Eir{\'{\i}}ksson and
Kenneth L. McMillan},
editor = {Pierre Wolper},
title = {Using Formal Verification/Analysis Methods on the Critical Path in
System Design: {A} Case Study},
booktitle = {Computer Aided Verification, 7th International Conference, Li{\`{e}}ge,
Belgium, July, 3-5, 1995, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {939},
pages = {367--380},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-60045-0\_63},
doi = {10.1007/3-540-60045-0\_63},
timestamp = {Sat, 20 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/EirikssonM95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/ClarkeGMZ95,
author = {Edmund M. Clarke and
Orna Grumberg and
Kenneth L. McMillan and
Xudong Zhao},
editor = {Bryan Preas},
title = {Efficient Generation of Counterexamples and Witnesses in Symbolic
Model Checking},
booktitle = {Proceedings of the 32st Conference on Design Automation, San Francisco,
California, USA, Moscone Center, June 12-16, 1995},
pages = {427--432},
publisher = {{ACM} Press},
year = {1995},
url = {https://doi.org/10.1145/217474.217565},
doi = {10.1145/217474.217565},
timestamp = {Tue, 17 Nov 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/ClarkeGMZ95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccad/McGeerMSSS95,
author = {Patrick C. McGeer and
Kenneth L. McMillan and
Alexander Saldanha and
Alberto L. Sangiovanni{-}Vincentelli and
Patrick Scaglia},
editor = {Richard L. Rudell},
title = {Fast discrete function evaluation using decision diagrams},
booktitle = {Proceedings of the 1995 {IEEE/ACM} International Conference on Computer-Aided
Design, {ICCAD} 1995, San Jose, California, USA, November 5-9, 1995},
pages = {402--407},
publisher = {{IEEE} Computer Society / {ACM}},
year = {1995},
url = {https://doi.org/10.1109/ICCAD.1995.480147},
doi = {10.1109/ICCAD.1995.480147},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/iccad/McGeerMSSS95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcad/BurchCLMD94,
author = {Jerry R. Burch and
Edmund M. Clarke and
David E. Long and
Kenneth L. McMillan and
David L. Dill},
title = {Symbolic model checking for sequential circuit verification},
journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
volume = {13},
number = {4},
pages = {401--424},
year = {1994},
url = {https://doi.org/10.1109/43.275352},
doi = {10.1109/43.275352},
timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcad/BurchCLMD94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan94,
author = {Kenneth L. McMillan},
editor = {David L. Dill},
title = {Hierarchical Representations of Discrete Functions, with Application
to Model Checking},
booktitle = {Computer Aided Verification, 6th International Conference, {CAV} '94,
Stanford, California, USA, June 21-23, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {818},
pages = {41--54},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-58179-0\_42},
doi = {10.1007/3-540-58179-0\_42},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/McMillan94,
author = {Kenneth L. McMillan},
editor = {Michael J. Lorenzetti},
title = {Fitting Formal Methods into the Design Cycle},
booktitle = {Proceedings of the 31st Conference on Design Automation, San Diego,
California, USA, June 6-10, 1994},
pages = {314--319},
publisher = {{ACM} Press},
year = {1994},
url = {https://doi.org/10.1145/196244.196392},
doi = {10.1145/196244.196392},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/McMillan94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/CollettGCBGMRSSZ94,
author = {Ronald Collett and
Mike Gianfagna and
Michel Courtoy and
Martin Baynes and
Johan Van Ginderdeuren and
Kenneth L. McMillan and
Stephen Ricca and
Alberto L. Sangiovanni{-}Vincentelli and
Steve Sapiro and
Naeem Zafar},
editor = {Michael J. Lorenzetti},
title = {Panel: Complex System Verification: The Challenge Ahead},
booktitle = {Proceedings of the 31st Conference on Design Automation, San Diego,
California, USA, June 6-10, 1994},
pages = {320},
publisher = {{ACM} Press},
year = {1994},
url = {https://doi.org/10.1145/196244.196394},
doi = {10.1145/196244.196394},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/CollettGCBGMRSSZ94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/daglib/0071856,
author = {Kenneth L. McMillan},
title = {Symbolic model checking},
publisher = {Kluwer},
year = {1993},
url = {https://doi.org/10.1007/978-1-4615-3190-6},
doi = {10.1007/978-1-4615-3190-6},
isbn = {978-0-7923-9380-1},
timestamp = {Tue, 23 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/daglib/0071856.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/chdl/ClarkeGHJLMN93,
author = {Edmund M. Clarke and
Orna Grumberg and
Hiromi Hiraishi and
Somesh Jha and
David E. Long and
Kenneth L. McMillan and
Linda A. Ness},
editor = {David Agnew and
Luc J. M. Claesen and
Raul Camposano},
title = {Verification of the Futurebus+ Cache Coherence Protocol},
booktitle = {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},
series = {{IFIP} Transactions},
volume = {{A-32}},
pages = {15--30},
publisher = {North-Holland},
year = {1993},
timestamp = {Thu, 03 Jan 2002 11:54:34 +0100},
biburl = {https://dblp.org/rec/conf/chdl/ClarkeGHJLMN93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/ClarkeMZFY93,
author = {Edmund M. Clarke and
Kenneth L. McMillan and
Xudong Zhao and
Masahiro Fujita and
Jerry Chih{-}Yuan Yang},
editor = {Alfred E. Dunlop},
title = {Spectral Transforms for Large Boolean Functions with Applications
to Technology Mapping},
booktitle = {Proceedings of the 30th Design Automation Conference. Dallas, Texas,
USA, June 14-18, 1993},
pages = {54--60},
publisher = {{ACM} Press},
year = {1993},
url = {https://doi.org/10.1145/157485.164569},
doi = {10.1145/157485.164569},
timestamp = {Tue, 17 Nov 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/ClarkeMZFY93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/BurchCMDH92,
author = {Jerry R. Burch and
Edmund M. Clarke and
Kenneth L. McMillan and
David L. Dill and
L. J. Hwang},
title = {Symbolic Model Checking: 10{\^{}}20 States and Beyond},
journal = {Inf. Comput.},
volume = {98},
number = {2},
pages = {142--170},
year = {1992},
url = {https://doi.org/10.1016/0890-5401(92)90017-A},
doi = {10.1016/0890-5401(92)90017-A},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/BurchCMDH92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/McMillan92,
author = {Kenneth L. McMillan},
editor = {Gregor von Bochmann and
David K. Probst},
title = {Using Unfoldings to Avoid the State Explosion Problem in the Verification
of Asynchronous Circuits},
booktitle = {Computer Aided Verification, Fourth International Workshop, {CAV}
'92, Montreal, Canada, June 29 - July 1, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {663},
pages = {164--177},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-56496-9\_14},
doi = {10.1007/3-540-56496-9\_14},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccd/McMillanD92,
author = {Kenneth L. McMillan and
David L. Dill},
title = {Algorithms for Interface Timing Verification},
booktitle = {Proceedings 1992 {IEEE} International Conference on Computer Design:
{VLSI} in Computer {\&} Processors, {ICCD} '92, Cambridge, MA,
USA, October 11-14, 1992},
pages = {48--51},
publisher = {{IEEE} Computer Society},
year = {1992},
url = {https://doi.org/10.1109/ICCD.1992.276208},
doi = {10.1109/ICCD.1992.276208},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/iccd/McMillanD92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pieee/ClarkeLM91,
author = {Edmund M. Clarke and
David E. Long and
Kenneth L. McMillan},
title = {A language for compositional specification and verification of finite
state hardware controllers},
journal = {Proc. {IEEE}},
volume = {79},
number = {9},
pages = {1283--1292},
year = {1991},
url = {https://doi.org/10.1109/5.97298},
doi = {10.1109/5.97298},
timestamp = {Tue, 21 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pieee/ClarkeLM91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcad/KurshanM91,
author = {Robert P. Kurshan and
Kenneth L. McMillan},
title = {Analysis of digital circuits through symbolic reduction},
journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
volume = {10},
number = {11},
pages = {1356--1371},
year = {1991},
url = {https://doi.org/10.1109/43.97615},
doi = {10.1109/43.97615},
timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcad/KurshanM91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccd/AkellaM91,
author = {Janaki Akella and
Kenneth L. McMillan},
title = {Synthesizing Converters Between Finite State Protocols},
booktitle = {Proceedings 1991 {IEEE} International Conference on Computer Design:
{VLSI} in Computer {\&} Processors, {ICCD} '91, Cambridge, MA,
USA, October 14-16, 1991},
pages = {410--413},
publisher = {{IEEE} Computer Society},
year = {1991},
url = {https://doi.org/10.1109/ICCD.1991.139932},
doi = {10.1109/ICCD.1991.139932},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/iccd/AkellaM91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dac/BurchCMD90,
author = {Jerry R. Burch and
Edmund M. Clarke and
Kenneth L. McMillan and
David L. Dill},
editor = {Richard C. Smith},
title = {Sequential Circuit Verification Using Symbolic Model Checking},
booktitle = {Proceedings of the 27th {ACM/IEEE} Design Automation Conference. Orlando,
Florida, USA, June 24-28, 1990},
pages = {46--51},
publisher = {{IEEE} Computer Society Press},
year = {1990},
url = {https://doi.org/10.1145/123186.123223},
doi = {10.1145/123186.123223},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/dac/BurchCMD90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/BurchCMDH90,
author = {Jerry R. Burch and
Edmund M. Clarke and
Kenneth L. McMillan and
David L. Dill and
L. J. Hwang},
title = {Symbolic Model Checking: 10{\^{}}20 States and Beyond},
booktitle = {Proceedings of the Fifth Annual Symposium on Logic in Computer Science
{(LICS} '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990},
pages = {428--439},
publisher = {{IEEE} Computer Society},
year = {1990},
url = {https://doi.org/10.1109/LICS.1990.113767},
doi = {10.1109/LICS.1990.113767},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/BurchCMDH90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/ClarkeLM89,
author = {Edmund M. Clarke and
David E. Long and
Kenneth L. McMillan},
title = {Compositional Model Checking},
booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science
{(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
pages = {353--362},
publisher = {{IEEE} Computer Society},
year = {1989},
url = {https://doi.org/10.1109/LICS.1989.39190},
doi = {10.1109/LICS.1989.39190},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/ClarkeLM89.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/podc/KurshanM89,
author = {Robert P. Kurshan and
Kenneth L. McMillan},
editor = {Piotr Rudnicki},
title = {A Structural Induction Theorem for Processes},
booktitle = {Proceedings of the Eighth Annual {ACM} Symposium on Principles of
Distributed Computing, Edmonton, Alberta, Canada, August 14-16, 1989},
pages = {239--247},
publisher = {{ACM}},
year = {1989},
url = {https://doi.org/10.1145/72981.72998},
doi = {10.1145/72981.72998},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/podc/KurshanM89.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
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.
last updated on 2024-04-21 18:14 CEST 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:
