default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "streamid:conf/acl2:"
download as .bib file
@inproceedings{DBLP:journals/corr/abs-2311-08854,
author = {David M. Russinoff},
editor = {Alessandro Coglio and
Sol Swords},
title = {A Formalization of Finite Group Theory: Part {III}},
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 = {33--49},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.5},
doi = {10.4204/EPTCS.393.5},
timestamp = {Fri, 22 Dec 2023 11:34:10 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08854.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 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08855.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08856,
author = {Matt Kaufmann and
J Strother Moore},
editor = {Alessandro Coglio and
Sol Swords},
title = {Advances in {ACL2} Proof Debugging Tools},
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 = {67--81},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.7},
doi = {10.4204/EPTCS.393.7},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08856.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08857,
author = {Ruben Gamboa and
Panagiotis Manolios and
Eric Whitman Smith and
Kyle Thompson},
editor = {Alessandro Coglio and
Sol Swords},
title = {Using Counterexample Generation and Theory Exploration to Suggest
Missing Hypotheses},
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 = {82--93},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.8},
doi = {10.4204/EPTCS.393.8},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08857.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08858,
author = {Alessandro Coglio and
Eric McCarthy and
Eric Whitman Smith},
editor = {Alessandro Coglio and
Sol Swords},
title = {Formal Verification of Zero-Knowledge Circuits},
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 = {94--112},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.9},
doi = {10.4204/EPTCS.393.9},
timestamp = {Tue, 30 Jul 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08858.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08859,
author = {Ankit Kumar and
Max von Hippel and
Panagiotis Manolios and
Cristina Nita{-}Rotaru},
editor = {Alessandro Coglio and
Sol Swords},
title = {Verification of GossipSub in ACL2s},
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 = {113--132},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.10},
doi = {10.4204/EPTCS.393.10},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08859.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08860,
author = {Andrew T. Walter and
Ankit Kumar and
Panagiotis Manolios},
editor = {Alessandro Coglio and
Sol Swords},
title = {Proving Calculational Proofs Correct},
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 = {133--150},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.11},
doi = {10.4204/EPTCS.393.11},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08860.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08861,
author = {Grant O. Passmore},
editor = {Alessandro Coglio and
Sol Swords},
title = {{ACL2} Proofs of Nonlinear Inequalities with Imandra},
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 = {151--160},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.12},
doi = {10.4204/EPTCS.393.12},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08861.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08862,
author = {David S. Hardin},
editor = {Alessandro Coglio and
Sol Swords},
title = {Verification of a Rust Implementation of Knuth's Dancing Links using
{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 = {161--174},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.13},
doi = {10.4204/EPTCS.393.13},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08862.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-08866,
author = {David M. Russinoff},
editor = {Alessandro Coglio and
Sol Swords},
title = {A Formalization of Finite Group Theory: Part {II}},
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 = {16--32},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393.4},
doi = {10.4204/EPTCS.393.4},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08866.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-2311-08373,
editor = {Alessandro Coglio and
Sol Swords},
title = {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},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.393},
doi = {10.4204/EPTCS.393},
timestamp = {Fri, 22 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-08373.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11694,
author = {Ruben Gamboa and
Woodrow Gamboa},
editor = {Rob Sumners and
Cuong Chau},
title = {All Prime Numbers Have Primitive Roots},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {9--18},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.3},
doi = {10.4204/EPTCS.359.3},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11694.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11695,
author = {Ruben Gamboa and
Alicia Thoney},
editor = {Rob Sumners and
Cuong Chau},
title = {Using {ACL2} To Teach Students About Software Testing},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {19--32},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.4},
doi = {10.4204/EPTCS.359.4},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11695.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11697,
author = {David A. Greve and
Jennifer A. Davis and
Laura R. Humphrey},
editor = {Rob Sumners and
Cuong Chau},
title = {A Mechanized Proof of Bounded Convergence Time for the Distributed
Perimeter Surveillance System {(DPSS)} Algorithm {A}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {33--47},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.5},
doi = {10.4204/EPTCS.359.5},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11697.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11698,
author = {Warren A. Hunt Jr. and
Vivek Ramanathan and
J Strother Moore},
editor = {Rob Sumners and
Cuong Chau},
title = {{VWSIM:} {A} Circuit Simulator},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {61--75},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.7},
doi = {10.4204/EPTCS.359.7},
timestamp = {Mon, 19 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11698.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11699,
author = {Jagadish Bapanapally and
Ruben Gamboa},
editor = {Rob Sumners and
Cuong Chau},
title = {A Free Group of Rotations of Rank 2},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {76--82},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.8},
doi = {10.4204/EPTCS.359.8},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11699.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11700,
author = {William D. Young},
editor = {Rob Sumners and
Cuong Chau},
title = {Modeling Asymptotic Complexity Using {ACL2}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {83--98},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.9},
doi = {10.4204/EPTCS.359.9},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11700.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11703,
author = {Mertcan Temel},
editor = {Rob Sumners and
Cuong Chau},
title = {Verified Implementation of an Efficient Term-Rewriting Algorithm for
Multiplier Verification on {ACL2}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {116--133},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.11},
doi = {10.4204/EPTCS.359.11},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11703.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11704,
author = {Andrew T. Walter and
Panagiotis Manolios},
editor = {Rob Sumners and
Cuong Chau},
title = {ACL2s Systems Programming},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {134--150},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.12},
doi = {10.4204/EPTCS.359.12},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11704.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11706,
author = {Alessandro Coglio and
Eric McCarthy and
Stephen J. Westfold and
Daniel Balasubramanian and
Abhishek Dubey and
Gabor Karsai},
editor = {Rob Sumners and
Cuong Chau},
title = {Syntheto: {A} Surface Language for {APT} and {ACL2}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {151--167},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.13},
doi = {10.4204/EPTCS.359.13},
timestamp = {Mon, 03 Mar 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11706.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11707,
author = {Alessandro Coglio},
editor = {Rob Sumners and
Cuong Chau},
title = {A Complex Java Code Generator for {ACL2} Based on a Shallow Embedding
of {ACL2} in Java},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {168--184},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.14},
doi = {10.4204/EPTCS.359.14},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11707.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11708,
author = {Alessandro Coglio},
editor = {Rob Sumners and
Cuong Chau},
title = {A Proof-Generating {C} Code Generator for {ACL2} Based on a Shallow
Embedding of {C} in {ACL2}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {185--201},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.15},
doi = {10.4204/EPTCS.359.15},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11708.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11709,
author = {David S. Hardin},
editor = {Rob Sumners and
Cuong Chau},
title = {Hardware/Software Co-Assurance using the Rust Programming Language
and {ACL2}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {202--216},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.16},
doi = {10.4204/EPTCS.359.16},
timestamp = {Thu, 28 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11709.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-13345,
author = {David M. Russinoff},
editor = {Rob Sumners and
Cuong Chau},
title = {Properties of the Hebrew Calendar},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {48--60},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.6},
doi = {10.4204/EPTCS.359.6},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-13345.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-13347,
author = {David M. Russinoff},
editor = {Rob Sumners and
Cuong Chau},
title = {A Formalization of Finite Group Theory},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {99--115},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.10},
doi = {10.4204/EPTCS.359.10},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-13347.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-2205-11103,
editor = {Rob Sumners and
Cuong Chau},
title = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359},
doi = {10.4204/EPTCS.359},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11103.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13761,
author = {David M. Russinoff},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Formal Verification of Arithmetic {RTL:} Translating Verilog to {C++}
to {ACL2}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {1--15},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.1},
doi = {10.4204/EPTCS.327.1},
timestamp = {Thu, 10 Dec 2020 15:19:59 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13761.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13762,
author = {Matt Kaufmann and
J Strother Moore},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Iteration in {ACL2}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {16--31},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.2},
doi = {10.4204/EPTCS.327.2},
timestamp = {Mon, 19 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13762.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13763,
author = {Sol Swords},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {New Rewriter Features in {FGL}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {32--46},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.3},
doi = {10.4204/EPTCS.327.3},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13763.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13764,
author = {Rob Sumners},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Computing and Proving Well-founded Orderings through Finite Abstractions},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {47--60},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.4},
doi = {10.4204/EPTCS.327.4},
timestamp = {Thu, 10 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13764.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13765,
author = {Mertcan Temel},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {RP-Rewriter: An Optimized Rewriter for Large Terms in {ACL2}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {61--74},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.5},
doi = {10.4204/EPTCS.327.5},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13765.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13766,
author = {Ruben Gamboa and
John R. Cowles and
Woodrow Gamboa},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Quadratic Extensions in {ACL2}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {75--86},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.6},
doi = {10.4204/EPTCS.327.6},
timestamp = {Thu, 10 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13766.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13767,
author = {Sol Swords},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Generating Mutually Inductive Theorems from Concise Descriptions},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {95--107},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.10},
doi = {10.4204/EPTCS.327.10},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13767.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13769,
author = {Alessandro Coglio},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Ethereum's Recursive Length Prefix in {ACL2}},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {108--124},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.11},
doi = {10.4204/EPTCS.327.11},
timestamp = {Thu, 10 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13769.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2009-13771,
author = {Alessandro Coglio and
Stephen J. Westfold},
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Isomorphic Data Type Transformations},
booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
pages = {125--141},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327.12},
doi = {10.4204/EPTCS.327.12},
timestamp = {Thu, 10 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-13771.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-2009-12521,
editor = {Grant O. Passmore and
Ruben Gamboa},
title = {Proceedings of the Sixteenth International Workshop on the {ACL2}
Theorem Prover and its Applications, Worldwide, Planet Earth, May
28-29, 2020},
series = {{EPTCS}},
volume = {327},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.327},
doi = {10.4204/EPTCS.327},
timestamp = {Thu, 10 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-12521.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04308,
author = {Alessandro Coglio},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {A Simple Java Code Generator for {ACL2} Based on a Deep Embedding
of {ACL2} in Java},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {1--17},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.1},
doi = {10.4204/EPTCS.280.1},
timestamp = {Mon, 03 Dec 2018 16:41:49 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04308.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04309,
author = {Mihir Parang Mehta},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Formalising Filesystems in the {ACL2} Theorem Prover: an Application
to {FAT32}},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {18--29},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.2},
doi = {10.4204/EPTCS.280.2},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04309.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04310,
author = {David A. Greve and
Andrew Gacek},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Trapezoidal Generalization over Linear Constraints},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {30--46},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.3},
doi = {10.4204/EPTCS.280.3},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04310.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04311,
author = {Sol Swords},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Incremental {SAT} Library Integration Using Abstract Stobjs},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {47--60},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.4},
doi = {10.4204/EPTCS.280.4},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04311.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04312,
author = {David S. Hardin and
Konrad Slind},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Using {ACL2} in the Design of Efficient, Verifiable Data Structures
for High-Assurance Systems},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {61--76},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.5},
doi = {10.4204/EPTCS.280.5},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04312.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04313,
author = {Alessandro Coglio and
Shilpi Goel},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Adding 32-bit Mode to the {ACL2} Model of the x86 {ISA}},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {77--94},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.6},
doi = {10.4204/EPTCS.280.6},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04313.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04314,
author = {Ruben Gamboa and
John R. Cowles},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {The Fundamental Theorem of Algebra in {ACL2}},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {98--110},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.8},
doi = {10.4204/EPTCS.280.8},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04314.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04315,
author = {Carl Kwan and
Mark R. Greenstreet},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {111--127},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.9},
doi = {10.4204/EPTCS.280.9},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04315.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04316,
author = {Carl Kwan and
Mark R. Greenstreet},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Convex Functions in ACL2(r)},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {128--142},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.10},
doi = {10.4204/EPTCS.280.10},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04316.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04317,
author = {Yan Peng and
Mark R. Greenstreet},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Smtlink 2.0},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {143--160},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.11},
doi = {10.4204/EPTCS.280.11},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04317.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04318,
author = {Sol Swords},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Hint Orchestration Using ACL2's Simplifier},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {164--171},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.13},
doi = {10.4204/EPTCS.280.13},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04318.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-05666,
author = {Matt Kaufmann},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {DefunT: {A} Tool for Automating Termination Proofs by Using the Community
Books (Extended Abstract)},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {161--163},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.12},
doi = {10.4204/EPTCS.280.12},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-05666.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1810-03762,
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280},
doi = {10.4204/EPTCS.280},
timestamp = {Mon, 03 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-03762.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/CoglioKS17,
author = {Alessandro Coglio and
Matt Kaufmann and
Eric Whitman Smith},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {A Versatile, Sound Tool for Simplifying Definitions},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {61--77},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.5},
doi = {10.4204/EPTCS.249.5},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/CoglioKS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/CowlesG17,
author = {John R. Cowles and
Ruben Gamboa},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {The Cayley-Dickson Construction in {ACL2}},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {18--29},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.2},
doi = {10.4204/EPTCS.249.2},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/CowlesG17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Goel17,
author = {Shilpi Goel},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {The x86isa Books: Features, Usage, and Future Plans},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {1--17},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.1},
doi = {10.4204/EPTCS.249.1},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Goel17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/KaufmannS17,
author = {Matt Kaufmann and
Sol Swords},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {Meta-extract: Using Existing Facts in Meta-reasoning},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {47--60},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.4},
doi = {10.4204/EPTCS.249.4},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KaufmannS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Russinoff17,
author = {David M. Russinoff},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {A Computationally Surveyable Proof of the Group Properties of an Elliptic
Curve},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {30--46},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.3},
doi = {10.4204/EPTCS.249.3},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Russinoff17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Sumners17,
author = {Rob Sumners},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems
and Applications},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {78--94},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.6},
doi = {10.4204/EPTCS.249.6},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Sumners17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Swords17,
author = {Sol Swords},
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {Term-Level Reasoning in Support of Bit-blasting},
booktitle = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
pages = {95--111},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.249.7},
doi = {10.4204/EPTCS.249.7},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Swords17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/SlobodovaJ17,
editor = {Anna Slobodov{\'{a}} and
Warren A. Hunt Jr.},
title = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover
and its Applications, Austin, Texas, USA, May 22-23, 2017},
series = {{EPTCS}},
volume = {249},
year = {2017},
url = {http://arxiv.org/abs/1705.00766},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/SlobodovaJ17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/ChauKH15,
author = {Cuong K. Chau and
Matt Kaufmann and
Warren A. Hunt Jr.},
editor = {Matt Kaufmann and
David L. Rager},
title = {Fourier Series Formalization in ACL2(r)},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {35--51},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.4},
doi = {10.4204/EPTCS.192.4},
timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
biburl = {https://dblp.org/rec/journals/corr/ChauKH15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Coglio15,
author = {Alessandro Coglio},
editor = {Matt Kaufmann and
David L. Rager},
title = {Second-Order Functions and Theorems in {ACL2}},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {17--33},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.3},
doi = {10.4204/EPTCS.192.3},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Coglio15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/CowlesG15,
author = {John R. Cowles and
Ruben Gamboa},
editor = {Matt Kaufmann and
David L. Rager},
title = {Perfect Numbers in {ACL2}},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {53--59},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.5},
doi = {10.4204/EPTCS.192.5},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/CowlesG15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Hardin15,
author = {David S. Hardin},
editor = {Matt Kaufmann and
David L. Rager},
title = {Reasoning About {LLVM} Code Using Codewalker},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {79--92},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.7},
doi = {10.4204/EPTCS.192.7},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Hardin15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/JainM15a,
author = {Mitesh Jain and
Panagiotis Manolios},
editor = {Matt Kaufmann and
David L. Rager},
title = {Proving Skipping Refinement with ACL2s},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {111--127},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.9},
doi = {10.4204/EPTCS.192.9},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/JainM15a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Moore15a,
author = {J Strother Moore},
editor = {Matt Kaufmann and
David L. Rager},
title = {Stateman: Using Metafunctions to Manage Large Terms Representing Machine
States},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {93--109},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.8},
doi = {10.4204/EPTCS.192.8},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Moore15a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/PengG15,
author = {Yan Peng and
Mark R. Greenstreet},
editor = {Matt Kaufmann and
David L. Rager},
title = {Extending {ACL2} with {SMT} Solvers},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {61--77},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.6},
doi = {10.4204/EPTCS.192.6},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/PengG15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/SwordsD15,
author = {Sol Swords and
Jared Davis},
editor = {Matt Kaufmann and
David L. Rager},
title = {Fix Your Types},
booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
pages = {3--16},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192.2},
doi = {10.4204/EPTCS.192.2},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/SwordsD15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/KaufmannR15,
editor = {Matt Kaufmann and
David L. Rager},
title = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015},
series = {{EPTCS}},
volume = {192},
year = {2015},
url = {https://doi.org/10.4204/EPTCS.192},
doi = {10.4204/EPTCS.192},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KaufmannR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/ChamarthiDM14,
author = {Harsh Raju Chamarthi and
Peter C. Dillinger and
Panagiotis Manolios},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Data Definitions in the {ACL2} Sedan},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {27--48},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.3},
doi = {10.4204/EPTCS.152.3},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/ChamarthiDM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/CowlesG14,
author = {John R. Cowles and
Ruben Gamboa},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Equivalence of the Traditional and Non-Standard Definitions of Concepts
from Real Analysis},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {89--100},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.8},
doi = {10.4204/EPTCS.152.8},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/CowlesG14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/DavisK14,
author = {Jared Davis and
Matt Kaufmann},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Industrial-Strength Documentation for {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {9--25},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.2},
doi = {10.4204/EPTCS.152.2},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/DavisK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/GamboaC14,
author = {Ruben Gamboa and
John R. Cowles},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Formal Verification of Medina's Sequence of Polynomials for Approximating
Arctangent},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {101--110},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.9},
doi = {10.4204/EPTCS.152.9},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/GamboaC14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/HardinDGM14,
author = {David S. Hardin and
Jennifer A. Davis and
David A. Greve and
Jedidiah R. McClurg},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Development of a Translator from {LLVM} to {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {163--177},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.13},
doi = {10.4204/EPTCS.152.13},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/HardinDGM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/HerasK14b,
author = {J{\'{o}}nathan Heras and
Ekaterina Komendantskaya},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {ACL2(ml): Machine-Learning for {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {61--75},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.5},
doi = {10.4204/EPTCS.152.5},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/HerasK14b.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/JoostenKU14,
author = {Sebastiaan J. C. Joosten and
Cezary Kaliszyk and
Josef Urban},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Initial Experiments with TPTP-style Automated Theorem Provers on {ACL2}
Problems},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {77--85},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.6},
doi = {10.4204/EPTCS.152.6},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/JoostenKU14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/KaufmannM14,
author = {Matt Kaufmann and
J Strother Moore},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Enhancements to {ACL2} in Versions 6.2, 6.3, and 6.4},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {1--7},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.1},
doi = {10.4204/EPTCS.152.1},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KaufmannM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/OLearyR14,
author = {John W. O'Leary and
David M. Russinoff},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Modeling Algorithms in SystemC and {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {145--162},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.12},
doi = {10.4204/EPTCS.152.12},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/OLearyR14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/PuriRHX14,
author = {Disha Puri and
Sandip Ray and
Kecheng Hao and
Fei Xie},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Using {ACL2} to Verify Loop Pipelining in Behavioral Synthesis},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {111--128},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.10},
doi = {10.4204/EPTCS.152.10},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/PuriRHX14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Selfridge14,
author = {Benjamin Selfridge},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {An {ACL2} Mechanization of an Axiomatic Framework for Weak Memory},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {129--144},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.11},
doi = {10.4204/EPTCS.152.11},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Selfridge14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/SelfridgeS14,
author = {Benjamin Selfridge and
Eric Smith},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Polymorphic Types in {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {49--59},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.4},
doi = {10.4204/EPTCS.152.4},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/SelfridgeS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/VerbeekS14,
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152},
doi = {10.4204/EPTCS.152},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/VerbeekS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7855,
author = {Matt Kaufmann and
J Strother Moore},
editor = {Ruben Gamboa and
Jared Davis},
title = {Enhancements to {ACL2} in Versions 5.0, 6.0, and 6.1},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {5--12},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.1},
doi = {10.4204/EPTCS.114.1},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7855.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7856,
author = {Caleb Eggensperger},
editor = {Ruben Gamboa and
Jared Davis},
title = {Proof Pad: {A} New Development Environment for {ACL2}},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {13--28},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.2},
doi = {10.4204/EPTCS.114.2},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7856.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7857,
author = {David A. Greve and
Konrad Slind},
editor = {Ruben Gamboa and
Jared Davis},
title = {A Step-Indexing Approach to Partial Functions},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {42--53},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.4},
doi = {10.4204/EPTCS.114.4},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7857.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7858,
author = {Shilpi Goel and
Warren A. Hunt Jr. and
Matt Kaufmann},
editor = {Ruben Gamboa and
Jared Davis},
title = {Abstract Stobjs and Their Application to {ISA} Modeling},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {54--69},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.5},
doi = {10.4204/EPTCS.114.5},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7858.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7859,
author = {Freek Verbeek and
Julien Schmaltz},
editor = {Ruben Gamboa and
Jared Davis},
title = {Verification of Building Blocks for Asynchronous Circuits},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {70--84},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.6},
doi = {10.4204/EPTCS.114.6},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7859.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7860,
author = {Lucas Helms and
Ruben Gamboa},
editor = {Ruben Gamboa and
Jared Davis},
title = {An Interpreter for Quantum Circuits},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {85--94},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.7},
doi = {10.4204/EPTCS.114.7},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7860.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7861,
author = {Jared Davis and
Sol Swords},
editor = {Ruben Gamboa and
Jared Davis},
title = {Verified {AIG} Algorithms in {ACL2}},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {95--110},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.8},
doi = {10.4204/EPTCS.114.8},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7861.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7862,
author = {Bernard van Gastel and
Julien Schmaltz},
editor = {Ruben Gamboa and
Jared Davis},
title = {A formalisation of {XMAS}},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {111--126},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.9},
doi = {10.4204/EPTCS.114.9},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7862.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7863,
author = {David S. Hardin and
Samuel S. Hardin},
editor = {Ruben Gamboa and
Jared Davis},
title = {{ACL2} Meets the {GPU:} Formalizing a CUDA-based Parallelizable All-Pairs
Shortest Path Algorithm in {ACL2}},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {127--142},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.10},
doi = {10.4204/EPTCS.114.10},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7863.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7875,
author = {Sebastiaan J. C. Joosten and
Bernard van Gastel and
Julien Schmaltz},
editor = {Ruben Gamboa and
Jared Davis},
title = {A Macro for Reusing Abstract Functions and Theorems},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {29--41},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.3},
doi = {10.4204/EPTCS.114.3},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7875.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1304-7123,
editor = {Ruben Gamboa and
Jared Davis},
title = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114},
doi = {10.4204/EPTCS.114},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7123.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1105-4394,
author = {Harsh Raju Chamarthi and
Peter C. Dillinger and
Matt Kaufmann and
Panagiotis Manolios},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Integrating Testing and Interactive Theorem Proving},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {4--19},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.1},
doi = {10.4204/EPTCS.70.1},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1105-4394.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4671,
author = {John R. Cowles and
Ruben Gamboa},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Verifying Sierpinski and Riesel Numbers in {ACL2}},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {20--27},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.2},
doi = {10.4204/EPTCS.70.2},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4671.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4672,
author = {Mike Dahlin and
Ryan Johnson and
Robert Bellarmine Krug and
Michael McCoyd and
William D. Young},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Toward the Verification of a Simple Hypervisor},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {28--45},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.3},
doi = {10.4204/EPTCS.70.3},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4672.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4673,
author = {Matt Kaufmann and
J Strother Moore},
editor = {David S. Hardin and
Julien Schmaltz},
title = {How Can {I} Do That with ACL2? Recent Enhancements to {ACL2}},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {46--60},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.4},
doi = {10.4204/EPTCS.70.4},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4673.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4674,
author = {Peter Reid and
Ruben Gamboa},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Implementing an Automatic Differentiator in {ACL2}},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {61--69},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.5},
doi = {10.4204/EPTCS.70.5},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4674.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4675,
author = {Peter{-}Michael Seidel},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier
with Redundant Feedback},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {70--83},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.6},
doi = {10.4204/EPTCS.70.6},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4675.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4676,
author = {Sol Swords and
Jared Davis},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Bit-Blasting {ACL2} Theorems},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {84--102},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.7},
doi = {10.4204/EPTCS.70.7},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4676.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1110-4677,
author = {Freek Verbeek and
Julien Schmaltz},
editor = {David S. Hardin and
Julien Schmaltz},
title = {Formal verification of a deadlock detection algorithm},
booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
pages = {103--112},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70.8},
doi = {10.4204/EPTCS.70.8},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4677.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1110-4473,
editor = {David S. Hardin and
Julien Schmaltz},
title = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
2011},
series = {{EPTCS}},
volume = {70},
year = {2011},
url = {https://doi.org/10.4204/EPTCS.70},
doi = {10.4204/EPTCS.70},
timestamp = {Tue, 16 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1110-4473.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/BoyerHH06,
author = {Robert S. Boyer and
Warren A. Hunt Jr.},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Function memoization and unique object representation for {ACL2} functions},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {81--89},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217992},
doi = {10.1145/1217975.1217992},
timestamp = {Tue, 23 Jun 2020 17:42:40 +0200},
biburl = {https://dblp.org/rec/conf/acl2/BoyerHH06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/CowlesG06,
author = {John R. Cowles and
Ruben Gamboa},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Unique factorization in {ACL2:} Euclidean domains},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {21--27},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217980},
doi = {10.1145/1217975.1217980},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/CowlesG06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Davis06,
author = {Jared Davis},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Memories: array-like records for {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {57--60},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217986},
doi = {10.1145/1217975.1217986},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Davis06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Davis06a,
author = {Jared Davis},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Reasoning about {ACL2} file input},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {117--126},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1218000},
doi = {10.1145/1217975.1218000},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Davis06a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/GamboaC06,
author = {Ruben Gamboa and
John R. Cowles},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Implementing a cost-aware evaluator for {ACL2} expressions},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {71--80},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217991},
doi = {10.1145/1217975.1217991},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/GamboaC06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/GordonHKR06,
author = {Michael J. C. Gordon and
Warren A. Hunt Jr. and
Matt Kaufmann and
James Reynolds},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {An embedding of the {ACL2} logic in {HOL}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {40--46},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217984},
doi = {10.1145/1217975.1217984},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/GordonHKR06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Greve06,
author = {David A. Greve},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Parameterized congruences in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {28--34},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217981},
doi = {10.1145/1217975.1217981},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Greve06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/HardinSY06,
author = {David S. Hardin and
Eric Whitman Smith and
William D. Young},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {A robust machine code proof framework for highly secure applications},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {11--20},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217978},
doi = {10.1145/1217975.1217978},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/HardinSY06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Hoare06,
author = {Tony Hoare},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {The ideal of verified software},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {61--62},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217988},
doi = {10.1145/1217975.1217988},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Hoare06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/HuntN06,
author = {Warren A. Hunt Jr. and
Serita M. Nelesen},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Phylogenetic trees in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {99--102},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217996},
doi = {10.1145/1217975.1217996},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/HuntN06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/HuntR06,
author = {Warren A. Hunt Jr. and
Erik Reeber},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {A SAT-based procedure for verifying finite state machines in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {127--135},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1218001},
doi = {10.1145/1217975.1218001},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/HuntR06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/KaufmannM06,
author = {Matt Kaufmann and
J Strother Moore},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Double rewriting for equivalential reasoning in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {103--106},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217997},
doi = {10.1145/1217975.1217997},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/KaufmannM06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/PikeSM06,
author = {Lee Pike and
Mark Shields and
John Matthews},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {A verifying core for a cryptographic language compiler},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {1--10},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217977},
doi = {10.1145/1217975.1217977},
timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/PikeSM06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Rager06,
author = {David L. Rager},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Adding parallelism capabilities to {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {90--94},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217994},
doi = {10.1145/1217975.1217994},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Rager06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Ray06,
author = {Sandip Ray},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Quantification in tail-recursive function definitions},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {95--98},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217995},
doi = {10.1145/1217975.1217995},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/Ray06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/ReeberS06,
author = {Erik Reeber and
Jun Sawada},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Combining {ACL2} and an automated verification tool to verify a multiplier},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {63--70},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217990},
doi = {10.1145/1217975.1217990},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/ReeberS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/SchmaltzB06,
author = {Julien Schmaltz and
Dominique Borrione},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Towards a formal theory of on chip communications in the {ACL2} logic},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {47--56},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217985},
doi = {10.1145/1217975.1217985},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/SchmaltzB06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/SwordsC06,
author = {Sol Swords and
William R. Cook},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Soundness of the simply typed lambda calculus in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {35--39},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217982},
doi = {10.1145/1217975.1217982},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/acl2/SwordsC06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/VaillancourtPF06,
author = {Dale Vaillancourt and
Rex L. Page and
Matthias Felleisen},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {{ACL2} in DrScheme},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {107--116},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217999},
doi = {10.1145/1217975.1217999},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/acl2/VaillancourtPF06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/acl2/2006,
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
publisher = {{ACM}},
year = {2006},
isbn = {0-9788493-0-2},
timestamp = {Tue, 23 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/acl2/2006.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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.
retrieved on 2025-03-13 09:33 CET from data curated 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:
