Effective race detection for event-driven programs
Veselin Raychev, Martin Vechev, et al.
OOPSLA 2013
We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures. Copyright © 2013 ACM.
Veselin Raychev, Martin Vechev, et al.
OOPSLA 2013
Nick Mitchell, Peter F. Sweeney
OOPSLA 2013
Suparna Bhattacharya, K. Gopinath, et al.
OOPSLA 2013
Veselin Raychev, Max Schäfer, et al.
OOPSLA 2013