Wed 28 Oct 2015 11:15 - 11:37 at Grand Station 1 - 1. Model Checking Chair(s): Julian Dolby

We present an efficient, modular, and feature-rich framework for automated generation and validation of complex structures, suitable for tasks that explore a large space of structured values. Our framework is capable of exhaustive, incremental, parallel, and memoized enumeration from not only finite but also infinite domains, while providing fine-grained control over the process. Furthermore, the framework efficiently supports the inverse of enumeration (checking whether a structure can be generated and fast-forwarding to this structure to continue the enumeration) and lazy enumeration (achieving exhaustive testing without generating all structures). The foundation of efficient enumeration lies in both direct access to encoded structures, achieved with well-known and new pairing functions, and dependent enumeration, which embeds constraints into the enumeration to avoid backtracking. Our framework defines an algebra of enumerators, with combinators for their composition that preserve exhaustiveness and efficiency. We have implemented our framework as a domain-specific language in Scala. Our experiments demonstrate better performance and shorter specifications by up to a few orders of magnitude compared to existing approaches.

Wed 28 Oct

oopsla2015
10:30 - 12:00: OOPSLA - 1. Model Checking at Grand Station 1
Chair(s): Julian DolbyIBM Research
oopsla201510:30 - 10:52
Talk
Anthony Widjaja LinYale-NUS College, Singapore, Matthew HagueRoyal Holloway University of London, UK, C.-H. Luke OngUniversity of Oxford, UK
Link to publication
oopsla201510:52 - 11:15
Talk
Brian DemskyUniversity of California at Irvine, USA, Patrick LamUniversity of Waterloo, Canada
Link to publication
oopsla201511:15 - 11:37
Talk
Ivan KurajMassachusetts Institute of Technology, USA, Viktor KunčakEPFL, Switzerland, Daniel JacksonMassachusetts Institute of Technology, USA
DOI
oopsla201511:37 - 12:00
Talk
Casper Svenning JensenAarhus University, Denmark, Anders MøllerAarhus University, Veselin RaychevETH Zurich, Switzerland, Dimitar DimitrovETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
DOI