About The Forum
Calendar 2017 Poster Sessions : Towards Reliable and Maintainable Constraint Solvers
Student Name : Andres Nötzli
Advisor : None
Advisor : None
Abstract:
Satisfiability modulo theories (SMT) solvers are constraint solvers often used for program verification and symbolic execution. State-of-the-art solvers implement hundreds of preprocessing rules in low-level programming languages to achieve good performance, which makes the preprocessing module complex and a common source of bugs. We propose a domain-specific language (DSL) for preprocessing rules that reduces the effort of implementing preprocessing rules and enables the production of proofs for the work done by the solver to increase the reliability and the maintainability of the solvers.
Bio:
Andres Nötzli is a third year PhD student in the Computer Science Department at Stanford University, advised by Prof. Clark Barrett and Prof. Dawson Engler. He is broadly interested in making software more reliable. His interests include programming languages, compilers, bug finding, and databases.
Satisfiability modulo theories (SMT) solvers are constraint solvers often used for program verification and symbolic execution. State-of-the-art solvers implement hundreds of preprocessing rules in low-level programming languages to achieve good performance, which makes the preprocessing module complex and a common source of bugs. We propose a domain-specific language (DSL) for preprocessing rules that reduces the effort of implementing preprocessing rules and enables the production of proofs for the work done by the solver to increase the reliability and the maintainability of the solvers.
Bio:
Andres Nötzli is a third year PhD student in the Computer Science Department at Stanford University, advised by Prof. Clark Barrett and Prof. Dawson Engler. He is broadly interested in making software more reliable. His interests include programming languages, compilers, bug finding, and databases.