@article(DBLP:journals/sttt/ArmandoMP09,
 author       = {Alessandro Armando and Jacopo Mantovani and Lorenzo Platania},
 year         = {2009},
 title        = {Bounded model checking of software using {SMT} solvers instead of {SAT} solvers},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {11},
 number       = {1},
 pages        = {69--83},
 doi          = {10.1007/s10009-008-0091-0},
)
@misc(smtlib-theories,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 title        = {{SMTLib 2.6 Theory Definitions}},
 url          = {https://smtlib.cs.uiowa.edu/theories.shtml},
)
@techreport(BarFT-RR-17,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2021},
 title        = {{The SMT-LIB Standard: Version 2.6}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 url          = {http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf},
)
@inproceedings(DBLP:conf/arith/BrainTRW15,
 author       = {Martin Brain and Cesare Tinelli and Philipp R{\"{u}}mmer and Thomas Wahl},
 year         = {2015},
 title        = {An Automatable Formal Semantics for {IEEE-754} Floating-Point Arithmetic},
 booktitle    = {22nd {IEEE} Symposium on Computer Arithmetic},
 publisher    = {{IEEE}},
 pages        = {160--167},
 doi          = {10.1109/ARITH.2015.26},
)
@inproceedings(DBLP:conf/osdi/CadarDE08,
 author       = {Cristian Cadar and Daniel Dunbar and Dawson R. Engler},
 year         = {2008},
 title        = {{KLEE:} Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs},
 editor       = {Richard Draves and Robbert van Renesse},
 booktitle    = {8th {USENIX} Symposium on Operating Systems Design and Implementation},
 publisher    = {{USENIX} Association},
 pages        = {209--224},
 url          = {http://www.usenix.org/events/osdi08/tech/full\_papers/cadar/cadar.pdf},
)
@inproceedings(CBMC,
 author       = {Edmund M. Clarke and Daniel Kroening and Flavio Lerda},
 year         = {2004},
 title        = {A Tool for Checking {ANSI-C} Programs},
 editor       = {Kurt Jensen and Andreas Podelski},
 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},
 publisher    = {Springer},
 pages        = {168--176},
 doi          = {10.1007/978-3-540-24730-2\_15},
)
@inproceedings(DBLP:conf/sigcse/Lister01,
 author       = {Raymond Lister},
 year         = {2001},
 title        = {Objectives and objective assessment in {CS1}},
 editor       = {Henry MacKay Walker and Ren{\'{e}}e A. McCauley and Judith L. Gersting and Ingrid Russell},
 booktitle    = {Proceedings of the 32rd {SIGCSE} Technical Symposium on Computer Science Education},
 publisher    = {{ACM}},
 pages        = {292--296},
 doi          = {10.1145/364447.364605},
)
@inproceedings(10.5555/2459936.2459938,
 author       = {Raymond Lister},
 year         = {2011},
 title        = {Concrete and Other Neo-Piagetian Forms of Reasoning in the Novice Programmer},
 booktitle    = {Proceedings of the Thirteenth Australasian Computing Education Conference - Volume 114},
 series       = {ACE '11},
 publisher    = {Australian Computer Society, Inc.},
 address      = {AUS},
 pages        = {9--18},
)
@inproceedings(z3,
 author       = {Leonardo de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3}: An Efficient {SMT} Solver},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@inproceedings(pathFinderI,
 author       = {Corina S. Pasareanu and Peter C. Mehlitz and David H. Bushnell and Gundy-Burlet, Karen and Michael Lowry and Suzette Person and Mark Pape},
 year         = {2008},
 title        = {Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing Nasa Software},
 series       = {ISSTA'08},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {15--26},
 doi          = {10.1145/1390630.1390635},
)
@inproceedings(SSA,
 author       = {Barry K. Rosen and Mark N. Wegman and F. Kenneth Zadeck},
 year         = {1988},
 title        = {Global Value Numbers and Redundant Computations},
 booktitle    = {Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series       = {POPL '88},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {12--27},
 doi          = {10.1145/73560.73562},
)
@inproceedings(DBLP:conf/ppig/TeagueL14,
 author       = {Donna Teague and Raymond Lister},
 year         = {2014},
 title        = {Blinded by their Plight: Tracing and the Preoperational Programmer},
 editor       = {Benedict du Boulay and Judith Good},
 booktitle    = {Proceedings of the 25th Annual Workshop of the Psychology of Programming Interest Group},
 publisher    = {Psychology of Programming Interest Group},
 pages        = {8},
 url          = {http://ppig.org/library/paper/blinded-their-plight-tracing-and-preoperational-programmer},
)
@inproceedings(pathFinderII,
 author       = {Willem Visser and Corina S. Pasareanu and Sarfraz Khurshid},
 year         = {2004},
 title        = {{T}est {I}nput {G}eneration with {J}ava {P}ath{F}inder},
 booktitle    = {Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis},
 series       = {ISSTA '04},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {97--107},
 doi          = {10.1145/1007512.1007526},
)