Model Checking in the Absence of Code, Model and Properties

Publication Type


Publication Date



Model checking is a major approach in ensuring software correctness. It verifies a model converted from code against some formal properties. However, difficulties and programmers ’ reluctance to formalize formal properties have been some hurdles to its widespread industrial adoption. Also, with the advent of commercial off-the-shelf (COTS) components provided by third party vendors, model checking is further challenged as often only a binary version of the code is provided by vendors. Interestingly, latest instrumentation tools like PIN and Valgrind have enable execution traces to be collected dynamically from a running program. In this preliminary study, we investigate what can be done with model checking tools when code, model and properties are not available and the only available input is execution traces. Specifically, we combine studies on learning automata from traces and learning temporal properties from traces. The preliminary study suggests an automatic way to discover bugs using model checking tools when only execution traces are available.


Software Engineering

Research Areas

Software Systems


5th Asian Symposium on Programming Languages and Systems (APLAS) (Poster Track)

City or Country


Additional URL