![]() ![]() So, in this example, we would start with creating one predicate \(p0(r, k)\) for the location where we enter foo over the variables r and k. When encoding the program as Horn clauses, we create one predicate for each control-location (basically for every place where a debugger could stop) over all program variables that are live (or can be observed with a debugger), and one Horn clause for each transition (or statement). Where we want to prove the assertion r=2*k. In a nutshell, the idea behind using Horn clauses is that we want a nice logic representation of the program where we don’t have to remove the loops, etc. Read more here.Ī more detailed overview with related work and a few nice pictures can be found in our CAV 2016 tool paper. Use a reasoning engine to prove the desired property and compute a certificate that the property holds or a counterexample that shows how it can be violated. ![]() ![]() Translate the simplified program and the property that needs to be verified into an intermediate form that makes various lemmas about the language explicit. Parse the input program and simplify it as much as possible. All these tools share a basic organization into three steps which we also used for building JayHorn: In particular for C, there is a set of tools, and even a tool competition. No threads, no dynamic class loading, no strange corner cases of static initialization.įirst, we looked at what’s out there. Java can be a nasty language (try yourself) so we set our goals humble: let’s focus on simple Java programs first. ![]() These bad states are specified by adding runtime assertions (where some assertions may be generated, e.g., that an object reference must not be Null before being accessed). We’ll talk about Horn clauses in a bit, but first: What exactly is a model checker for Java? For us, this is a program that tries to find a proof that certain bad states in a Java program are never reachable. Teme came up with that name because he was working on SeaHorn (C Horn clauses) already. The first thing you need is a catchy name: JayHorn. So we decided to build a model checker for Java programs. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |