Model Checking ProgramswithJava PathFinder: Model Checking Programs with Java PathFinder Willem Visser Peter Mehlitz NASA Ames Research Center


Motivation: Motivation 1997 – Deep Space 1 Remote Agent 1999 – Honeywell DEOS IMA O/S Model extraction by hand doesn’t scale Automated Program Model Checking Translation-based model checking is only has good as the target model checker Java to PROMELA translation for SPIN


Program Model Checking: Program Model Checking 10 years ago Almost no one did it 5 years ago Just a handful of tools existed Now BANDERA, BLAST, CBMC, dSPIN, JPF, MAGIC, SLAM, SPIN 4, Verisoft, CMC, ZING, etc.


Overview: Overview What is JPF? A model checker for Java Bytecode Getting Started with JPF Downloading, Installation and Running Examples Part 1 Deadlock in the Remote Agent K9 Rover Internal workings of JPF Model Java Interface Listeners Dynamic Partial-order reductions Choice Generators Extensions Regression tests (JUnit Integration) Examples Part 2 Stoned Hippies in three variations Race Detection Numeric Exceptions Partial Trace Analysis Symbolic Execution How we spent the summer! Abstractions Decision Procedure Extensions User Interface Analysis Java Static Analysis 9h00 – 10h30 11h00 – 13h00


What is Java PathFinder (1): What is Java PathFinder (1) explicit state model checker for Java bytecode focus is on finding bugs in Java programs concurrency related: deadlocks, (races), missed signals etc. Java runtime related: unhandled exceptions, heap usage, (cycle budgets) but also: complex application specific assertions


What is JPF (2): What is JPF (2) goal is to avoid modeling effort (check the real program), or at least use a real programming language for complex models implies that the main challenge is scalability JPF uses a variety of scalability enhancing mechanisms user extensible state abstraction & matching on-the-fly partial order reduction configurable search strategies: "find the bug before you run out of memory" user definable heuristics (searches, choice generators) key issue is configurable extensibility: overcome scalability constraints with suitable customization (using heuristics)


Key Points: Key Points Models can be infinite state Unbounded objects, threads,… Depth-first state generation (explicit-state) Verification requires abstraction Handle full Java language but only for closed systems cannot directly handle native code no Input/output through GUIs, files, Networks, … Must be modeled by java code instead Allows Nondeterministic Environments JPF traps special nondeterministic methods Checks for User-defined assertions, deadlock and user-specified properties


JPF Status: JPF Status developed at the Robust Software Engineering Group at NASA Ames Research Center currently in it’s fourth development cycle v1: Spin/Promela translator - 1999 v2: backtrackable, state matching JVM - 2000 v3: extension infrastructure (listeners, MJI) - 2004 v4: symbolic execution, choice generators - 4Q 2005 open sourced since 04/2005 under NOSA 1.3 license: it’s a first: no NASA system development hosted on public site before 11100 downloads since publication 04/2005


Getting and Installing JPF: Getting and Installing JPF Getting JPF svn co https://svn.sourceforge.net/svnroot/javapathfinder javapathfinder Compiling JPF Go to the JPF root directory Type build-tools/bin/ant Compiles JPF Adding “run-tests” will also run the regression tests The Eclipse Route Get Eclipse 3.2 www.eclipse.org Install Subclipse Goto: Help – Software Updates – Find and Install – Select New Features Type the following in the url field: http://subclipse.tigris.org/update_1.2.x Follow the instructions Create a new SVN project by selecting “Checkout Projects from SVN” Create a new repository for https://svn.sourceforge.net/svnroot/javapathfinder Select trunk It will automatically download and compile in Eclipse Hint If you ever run JPF from outside the JPF project then put a copy of default.properties in the build/jpf/gov/nasa/jpf directory – otherwise you’ll get a vm.class error at initialization


How To Run JPF: How To Run JPF generally speaking: like a VM (“java” replacement): > bin/jpf BUT: lots of configuration (classes) and parameterization (booleans, integers etc.) JPF is an open system need for flexible, extensible configuration system quite powerful, but can be somewhat confusing


JPF Configuration: JPF Configuration


Some Examples: Some Examples Remote Agent K9 Rover (‘real’ model, size)


Remote Agent: Remote Agent “oldclassic.java” Simplified version of the deadlock encountered in the Remote Agent Fixing oldclassic! Or rather trying to fix…


K9 Rover: K9 Rover Executes flexible plans for autonomy branching on state / temporal conditions Multi-threaded system communication through shared variables synchronization through mutexes and condition variables Main functionality: 8KLOC, C++/JAVA commands plans Exec Executive CondChecker Database ActionExec TempChecker


Directory Structure: Directory Structure


Under the Hood - Toplevel Structure: Under the Hood - Toplevel Structure two major concepts: Search and VM Search is the VM driver and Property evaluator VM is the state generator


Under the Hood - Search: Under the Hood - Search


Extending JPF - Listeners: Extending JPF - Listeners preferred way of extending JPF: ‘Listener’ variant of the Observer pattern - keep extensions out of the core classes listeners can subscribe to Search and VM events


Extending JPF - SearchListener: Extending JPF - SearchListener public interface SearchListener {  /* got the next state */   void stateAdvanced (Search search);  /* state was backtracked one step */  void stateBacktracked (Search search);    /* a previously generated state was restored     (can be on a completely different path) */  void stateRestored (Search search);    /* JPF encountered a property violation */   void propertyViolated (Search search);    /* we get this after we enter the search loop, but BEFORE the first forward */   void searchStarted (Search search);    /* there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application */ void searchConstraintHit (Search search);    /* we're done, either with or without a preceeding error */  void searchFinished (Search search); }


Extending JPF - VMListener: Extending JPF - VMListener public interface VMListener {   void instructionExecuted (JVM vm); // VM has executed next instruction   void threadStarted (JVM vm); // new Thread entered run() method     void threadTerminated (JVM vm); // Thread exited run() method     void classLoaded (JVM vm); // new class was loaded     void objectCreated (JVM vm); // new object was created     void objectReleased (JVM vm); // object was garbage collected     void gcBegin (JVM vm); // garbage collection mark phase started     void gcEnd (JVM vm); // garbage collection sweep phase terminated     void exceptionThrown (JVM vm); // exception was thrown   void nextChoice (JVM vm); // choice generator returned new value }


Extending JPF - Listener Example: Extending JPF - Listener Example public class HeapTracker extends GenericProperty implements VMListener, SearchListener { class PathStat { .. int heapSize = 0; .. } // helper to store additional state info PathStat stat = new PathStat(); Stack pathStats = new Stack(); public boolean check (JVM vm, Object arg) { // GenericProperty return (stat.heapSize <= maxHeapSizeLimit); } public void stateAdvanced (Search search) { // SearchListener if (search.isNewState()) {.. pathStats.push(stat); stat = (PathStat)stat.clone(); .. } public void stateBacktracked (Search search) { // SearchListener .. if (!pathStats.isEmpty()) stat = (PathStat) pathStats.pop(); } public void objectCreated (JVM vm) {.. // VMListener ElementInfo ei = vm.getLastElementInfo(); ..stat.heapSize += ei.getHeapSize(); .. } public void objectReleased (JVM vm) { // VMListener ElementInfo ei = vm.getLastElementInfo(); ..stat.heapSize -= ei.getHeapSize(); .. } ... }


Extending JPF - Listener Configuration: Extending JPF - Listener Configuration listeners are usually configured, not hard coded per configuration file: search.listener = MySearchListener vm.listener = MyVMListener jpf.listener = MyCombinedListener:MySecondListener... per command line: jpf ... +jpf.listener=MyCombinedListener ... hard coded: MyListener listener= new MyListener(..); .. Config config = JPF.createConfig( args); JPF jpf = new JPF( config); jpf. addSearchListener (listener); jpf. addVMListener ( listener); jpf.run(); ..


Going Native - Model Java Interface: Going Native - Model Java Interface JPF is a state-tracking JVM, running on top of a general JVM Java Native Interface (JNI) analogy: “execute one level lower” Model Java Interface (MJI): execute in the host VM that runs JPF itself


MJI - Why?: MJI - Why? one obvious reason: running native Java methods in JPF (otherwise we couldn’t run apps using standard libraries, which have lots of native methods) specific use of native methods: interface library methods to JPF runtime system (e.g. java.lang.Thread -> ThreadInfo) enables usage of specialized verification API in app, interfacing to JPF functionality: int input = gov.nasa.jpf.jvm.Verify.randomInt(10); but also useful for scalability reasons native methods can save state space native methods are executed atomically native methods execute much faster example: java.io.RandomAccessFile


MJI - Components: MJI - Components Model class: has native method declaration, executed by JPF NativePeer class: native method implementation, executed by JVM MJIEnv: native method calling context (to get back to JPF)


MJI - How: MJI - How


MJI - Example: MJI - Example application calls method to intercept .. System.out.println(“a message”); model class declares the method we want to intercept (doesn’t have to be native), is executed by JPF public class PrintStream .. { .. public void println (String s) {..} // usually native method } native peer has the method implementation that gets executed by host VM (not simulated by JPF) class JPF_java_io_PrintStream { .. public static void println__Ljava_lang_String_2 (MJIEnv env,int objRef, int strRef) { env.getVM().println(env.getStringObject(strRef)); } } 0: getstatic #2 3: ldc #3 5: invokevirtual #4


Scalability - Partial Order Reduction: Scalability - Partial Order Reduction concurrency is major contributor to state space explosion reduction of thread interleavings is paramount for scalability JPF employs on-the-fly Partial Order Reduction mechanism leveled approach that makes use of JVM instruction set and infrastructure (memory management) completely at runtime (on-the-fly)


POR - Scheduling Relevance: POR - Scheduling Relevance


POR - Shared Objects: POR - Shared Objects to detect races, we have to identify read/write access to objects that are visible from different threads expensive operation, BUT: can piggyback on garbage collection two phase approach: mark root set with thread id (statics are shared by default) traverse marked objects - if another thread id is reached, mark as shared problem: GC based on reachability, not accessibility -> need to break on certain fields (Thread.group->ThreadGroup.threads)


Choice Generator Motivation: Choice Generator Motivation


JPF Perspective: JPF Perspective State consists of 2 main components, the state of the JVM and the current and next choice Generator (i.e. the objects encapsulating the choice enumeration that produces new transitions) Transition is the sequence of instructions that leads from one state. There is no context within a transition, it's all in the same thread. There can be multiple transitions leading out of one state Choice is what starts a new transition. This can be a different thread, i.e. scheduling choice, or different “random” data value.


Role of Choices: Role of Choices In other words, possible existence of Choices is what terminates the last Transition, and selection of a Choice value precedes the next Transition. The first condition corresponds to creating a new ChoiceGenerator, and letting the SystemState know about it. The second condition means to query the next choice value from this ChoiceGenerator (either internally within the JVM, or in an instruction or native method).


Extensions: Extensions JPF was built to be extended Architecture is such that the core classes can be left alone when doing an extension Add code to the “extensions” directory that follows the same layout as the core classes Numeric Extension to check for errors such as Overflow Most of this extension was provided by Aleksandar Milicevic and Sasa Misailovic from UIUC


Regression Tests with JUnit: Regression Tests with JUnit


JUnit Example: JUnit Example package gov.nasa.jpf.mc; import org.junit.Test; import org.junit.runner.JUnitCore; import gov.nasa.jpf.jvm.TestJPF; public class TestOldClassicJPF extends TestJPF { static final String TEST_CLASS = "gov.nasa.jpf.mc.oldclassic"; public static void main (String[] args) { JUnitCore.main("gov.nasa.jpf.mc.TestOldClassicJPF"); } @Test public void testDFSearch () { String[] args = { TEST_CLASS }; runJPFDeadlock(args); } @Test public void testBFSHeuristic () { String[] args = { "+search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch", "+search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic", TEST_CLASS }; runJPFDeadlock(args); } }


TestJPF: TestJPF Extends junit.Assert Interface methods runJPFDeadlock(args) Expects a deadlock runJPFassertionError(args) Expects an assertion violation runJPFnoAssertionError(args) Don’t want to see an assertion violation runJPFException(args) Expects an exception runJPFnoException(args) Don‘t want to see an exception


More Examples: More Examples Stoned Hippies Regular version Using MJI Using a Listener Race Detection A more sophisticated use of a Listener Numeric Extensions With Junit integration Partial Trace Analysis Recording a path and then re-analyze from the end of the path


Stoned Hippies: Stoned Hippies Germany Netherlands


Stoned Hippies: Stoned Hippies Germany Netherlands 2


Stoned Hippies: Stoned Hippies Germany Netherlands 3


Stoned Hippies: Stoned Hippies Germany Netherlands 8


Stoned Hippies: Stoned Hippies Germany Netherlands 19


Symbolic Execution: Symbolic Execution Explicit-state model checking cannot handle large data domains Want to generate test cases for systems that manipulate complex data structures Collaborators Corina Pasareanu Sarfraz Khurshid Saswat Anand


Concrete Execution Path (example): Concrete Execution Path (example) x = 1, y = 0 1 >? 0 x = 1 + 0 = 1 y = 1 – 0 = 1 x = 1 – 1 = 0 0 – 1 >? 0 int x, y; if (x > y) { x = x + y; y = x – y; x = x – y; if (x – y > 0) assert(false); }


Symbolic Execution Tree (example): Symbolic Execution Tree (example) x = X, y = Y int x, y; if (x > y) { x = x + y; y = x – y; x = x – y; if (x – y > 0) assert(false); }


Example: Example class Node { int elem; Node next; Node swapNode() { if (next != null) if (elem > next.elem) { Node t = next; next = t.next; t.next = this; return t; } return this; } }


Challenges in Generalizing Symbolic Execution: Challenges in Generalizing Symbolic Execution how to handle fields in dynamic structures? how to handle aliasing? how to generate tests? satisfy criteria satisfy precondition are inequivalent


Generalized Symbolic Execution: Generalized Symbolic Execution model checker generates and explores “symbolic” execution tree non-determinism handles aliasing explore different heap configurations explicitly concurrency off-the-shelf decision procedures check path conditions lazy initialization initializes program’s inputs on an “as-needed” basis no a priori bound on input sizes preconditions to initialize inputs only with valid values


Algorithm (lazy initialization): Algorithm (lazy initialization) to symbolically execute a method create input objects with uninitialized fields execute! follow mainly Java semantics initialize fields “as-required” add constraints to path condition


Algorithm (aliasing): Algorithm (aliasing) when method execution accesses field f if (f is uninitialized) { if (f is reference field of type T) { non-deterministically initialize f to  null  a new object of class T (with uninitialized fields)  an object created during prior field initialization (alias) } if (f is numeric/string field) initialize f to a new symbolic value }


Algorithm (illustration): Algorithm (illustration) consider executing next = t.next;


Implementation via Instrumentation: program instrumentation counterexample(s)/test suite [heap+constraint+thread scheduling] Implementation via Instrumentation model checking decision procedure instrumented program correctness specification continue/ backtrack state: original program


Testing with Symbolic Execution: Testing with Symbolic Execution Focus on programs that manipulate complex data Java container classes, e.g. java.util.TreeMap Black box test input generation Using structural invariants Using API calls With symbolic data, i.e. kind-of gray-box White box Completely symbolic execution over structures


Red-Black Trees: Red-Black Trees (1) The root is BLACK (2) Red nodes can only have black children (3) All paths from a node to its leaves contain the same number of black nodes. Self-balancing Binary Search Trees Java TreeMap Implementation (4) Acyclic (5) Consistent Parents repOk(): conditions (1)-(5)


repOk() Fragment: repOk() Fragment boolean repOk(Entry e) { // root has no parent, root is black,… // RedHasOnlyBlackChildren workList = new LinkedList(); workList.add(e); while (!workList.isEmpty()) { Entry current=(Entry)workList.removeFirst(); Entry cl = current.left; Entry cr = current.right; if (current.color == RED) { if(cl != null && cl.color == RED) return false; if(cr != null && cr.color == RED) return false; } if (cl != null) workList.add(cl); if (cr != null) workList.add(cr); } // equal number of black nodes on left and right sub-tree… return true; }


Black-box TIG Symbolic Execution : Black-box TIG Symbolic Execution Symbolic execution of repOk() Generate new structures only when repOk() returns true Limit the size of the structures generated Only correct structures will be generated repOk() returns true after all nodes in the tree have been visited, hence they must all be concrete symbolic (partial) structures can fail repOk() Similar to Korat Not based on symbolic execution Cannot deal with constraints on primitive data Korat uses custom algorithms and is much faster


Symbolic Execution of repOk() Example: Symbolic Execution of repOk() Example public static boolean repOk() { if (root == null) return true; if (root.color == RED) return false; …


White-box TIG Symbolic Execution: White-box TIG Symbolic Execution Consider code coverage criterion when generating test inputs Use repOk() as a precondition during symbolic execution of source code


repOk() x 2abstract and concrete: repOk() x 2 abstract and concrete Symbolic Execution of Code During Lazy Initialization check Abstract repOk() When coverage is achieved, solve the symbolic constraints to create concrete inputs Concretize inputs by symbolic execution of Concrete repOk() over symbolic structures - as with Black-box TIG -


Abstract repOk(): Abstract repOk() Eliminate symbolic structures that cannot be converted to a concrete structure that satisfy repOk() Can accept symbolic structures that could lead to illegal concrete structures, i.e. it is conservative Abstract RepOk() can return TRUE, FALSE or Don’t Know if FALSE, eliminate structure if TRUE or Don’t Know, continue ... Example: (2) Red nodes have only black children. FALSE TRUE Don’t Know


White-box TIG: cover branches in deleteEntry(Entry p): White-box TIG: cover branches in deleteEntry(Entry p) /* precondition: p.repOk() */ private void deleteEntry(Entry p) { if (p.left != null && p.right != null) { Entry s = successor(p); swapPosition(s, p); } Entry replacement = (p.left != null ? p.left : p.right); if (replacement != null) { replacement.parent = p.parent; if (p.parent == null) root = replacement; else if (p == p.parent.left) { p.parent.left = replacement; } else p.parent.right = replacement; p.left = p.right = p.parent = null; if (p.color == BLACK) fixAfterDeletion(replacement); ...


Symbolic Execution for white-box TIG: Symbolic Execution for white-box TIG


API Based Testing: API Based Testing SUT ENV (m,n) m is the seq. length of API calls & n is the number of values used in the parameters of the calls API … put(v) del(v) Evaluate different techniques for selecting test-cases from ENV(m,n) to obtain maximum coverage


Framework: Framework SUT with minor instrumentation ENV TestListener Abstraction Mapping + State Storage Coverage Manager JPF


Environment Skeleton: Environment Skeleton M : sequence length N : parameter values A : abstraction used for (int i = 0; i < M; i++) { int x = Verify.random(N - 1); switch (Verify.random(1)) { case 0: put(x); break; case 1: remove(x); break; } } Verify.ignoreIf(checkStateMatch());


Symbolic Environment Skeleton: Symbolic Environment Skeleton M : sequence length A : abstraction used for (int i = 0; i < M; i++) { SymbolicInteger x = new SymbolicInteger(“X“+i); switch (Verify.random(1)) { case 0: put(x); break; case 1: remove(x); break; } } Verify.ignoreIf(checkStateMatch());


Sample Output: Sample Output Test case number 77 for '15,L+R+P-REDroot': put(0);put(4);put(5);put(1);put(2);put(3);remove(4); Unique ID for the test Branch Number Predicate Values Test-case to achieve above coverage Test case number 7 for '32,L-R-P+RED': X2(0) == X1(0) && X2(0) < X0(1) && X1(0) < X0(1) put(X0);put(X1);remove(X2); Test case number 7 for '32,L-R-P+RED': put(1);put(0);remove(0); Concrete Symbolic Path Condition with solutions Symbolic TC


Subsumption Checking: Subsumption Checking x1 x2 x3 x4 x5 + x1 > x2 & x2 > x3 & x2 x1 x1 x2 x3 x4 x5 + x1 > x2 & x2 > x3 & x2 x1 If only it was this simple!


Existential Elimination: Existential Elimination x1 x2 x3 x4 x5 PC s1 s3 & s4 s1 s1 s4 s2 s3 s5 +  s1,s2,s3,s4,s5 such that x1 = s1 & x2 = s4 & x3 = s3 & x4 = s5 & x5 = s2 & PC x1 > x2 & x2 > x3 & x2 x1


Results from ISSTA 2006 Paper: Results from ISSTA 2006 Paper We compared the following techniques (1st 3 are exhaustive; last 2 lossy) Traditional Model Checking Model Checking using Symmetry Reductions Symbolic Execution Model Checking using Abstract Matching on the shape of the containers Random Testing Using the following container classes Binary Tree Fibonacci Heap Binomial Heap Tree Map In how well they achieve Statement coverage Predicate coverage As we increase the length of the sequence of API calls For the concrete cases we also increase the number of parameters to be the same as the API calls We found the following general result Traditional Model Checking failed on all but the most trivial tasks (i.e. statement coverage) Model Checking with Symmetry reductions worked much better here (scaled to much larger sequence lengths) Symbolic Execution worked the best of the Exhaustive techniques (got optimal coverage in a number of cases) – in one case one needed a sequence length of 14 calls to obtain branch coverage and symbolic execution could do it Lossy techniques could obtain optimal Predicate coverage Shape abstractions worked better than random selection but only just See examples/issta2006 folder under the SVN repository to reproduce the experiments


Symbolic Execution Demo: Symbolic Execution Demo Start by Running Saswat Anand’s symbolic instrumenter on the SwapValues.java File Then run it through JPF using symbolic execution We will use CVC-Lite as a decision since it is the only decision procedure that currently compiles under Windows!


JPF Symbolic Execution - BEFORE: JPF Symbolic Execution - BEFORE Omega Interface Formula satisfiable/unsatisfiable Omega Java Version JPF


JPF Symbolic Execution - NOW: JPF Symbolic Execution - NOW Generic Decision Procedure Interface Formula satisfiable/unsatisfiable Omega Maryland JPF CVCLite Stanford Yices SRI STP Stanford Collaborator Saswat Anand


Communication Methods: Communication Methods Issue JPF and the Interface code is in Java Decision procedures are not in Java, mainly C/C++ code Various different ways of communication Native Using JNI to call the code directly Pipe Start a process and pipe the formulas and results back and forth Files Same as Pipe but now use files as communication method


Optimization using Tables: Optimization using Tables JPF State Path Condition: X > Y & Z > X & … JPF State Path Condition: pc100 Outside JPF Table of PCs – … X > Y Z > X X >Y & Z > X & … 45 46 100 … …


Optimization – Run DPs incrementally: Optimization – Run DPs incrementally Some decision procedures support running in a incremental mode where you do not have to send the whole formula at a time but just what was added and/or removed. CVCLite Yices


Decision Procedure Options: Decision Procedure Options +symbolic.dp= omega.file omega.pipe omega.native omega.native.inc …inc - with table optimization yices.native yices.native.inc yices.native.incsolve …incsolve - Table optimization and incremental solving cvcl.file cvcl.pipe cvcl.native cvcl.native.inc cvcl.native.incsolve stp.native If using File or Pipe one must also set Symbolic..exe to the executable binary for the DP For the rest one must set LD_LIBRARY_PATH to where the DP libraries are stored Extensions/symbolic/CSRC Currently everything works under Linux and only CVCLite under Windows Symbolic.cvclite.exe = cvclite.exe must be set with CVClite.exe in the Path


Results TCAS: Results TCAS


Results TreeMap: Results TreeMap STP took > 1 hour


State Matching in JPF: State Matching in JPF VM State Matchable + Restorable Stored State (hashed) Matchable compression Collaborator Peter Dillinger


Old Architecture: Old Architecture StateSet int[] bool


New Architecture: New Architecture VM/Search DefaultBacktracker VM bool int[]


Old Scheme in the New Architecture: Old Scheme in the New Architecture VM/Search DefaultBacktracker FullStateSet int[] set bool int[] Collapsing (de)Serializer int[]


New Architecture: New Architecture VM/Search CollapsingRestorer FilteringSerializer DefaultBacktracker VM bool int[] objects This is the default setting for JPF at the moment: vm.backtracker.class = gov.nasa.jpf.jvm.DefaultBacktracker vm.restorer.class = gov.nasa.jpf.jvm.CollapsingRestorer vm.serializer.class = gov.nasa.jpf.filter.FilteringSerializer vm.storage.class = gov.nasa.jpf.jvm.JenkinsStateSet


FilteringSerializer : FilteringSerializer By default captures the fundamental VM state i.e. with all known unnecessary information removed Can also ignore fields based on annotations @FilterField(condition="foo") static int mods = 0; Filters the field if the condition is true, the condition statement is optional Does garbage collection after erasing/filtering fields Does heap canonicalization to give (heap) symmetry reductions By default it eliminates fields like “modCount” from the java.util classes Otherwise even the most trivial example will have an infinite state space See the ModCount.java demo Can easily specify shape abstractions by filtering out all non-reference fields from an object This will allow automatically doing the ISSTA 2006 shape abstraction


New Architecture Revisited - Abstraction: New Architecture Revisited - Abstraction VM/Search CollapsingRestorer AbstractingSerializer DefaultBacktracker VM bool int[] objects This is the setting for the above configuration: vm.backtracker.class = gov.nasa.jpf.jvm.DefaultBacktracker vm.restorer.class = gov.nasa.jpf.jvm.CollapsingRestorer vm.serializer.class = gov.nasa.jpf.abstraction.abstractingSerializer vm.storage.class = gov.nasa.jpf.jvm.JenkinsStateSet


AbstractingSerializer: AbstractingSerializer First does FilteringSerializer Also gives the ability to specify abstractions that are not just deleting part of the state (what FilteringSerializer does) The parts of the VM state is converted to an abstract state graph node Graph based abstractions can then be performed Other examples include Rounding floating point to the nearest 0.001 Include only difference of two variables Ignore ordering of values Adds support for sets modulo permutations, which is currently only used for specifying the set of threads i.e. this now gives thread symmetry reductions


Examples: Examples K9 revisited Filtering visits many less states Abstraction doesn’t give anything here since there is no thread symmetry to exploit ModCount example Infinite state without filtering Dining Philosophers Regular setup cannot go beyond 5 philosophers Abstraction is better than Filtering here, but takes longer There is a lot of thread symmetries here to exploit Filtering Fields Show the effect of removing fields through annotations


User-Interface Model Checking: User-Interface Model Checking Extension to JPF to deal with UIs directly See extensions/ui directory Deals with swing and awt New JPF front-end for querying a UI to find its structure Allows the scripting of nondeterministic executions using the structure of the UI Very simple language right now but will be extended in the future This is work in progress, but it has been able to find a serious problem in a prototype launch sequencer to be used in the launch vehicle for the ARES project (going back to the Moon and on to Mars) TestMe demo Run TestMe by itself and see if you can find a bug! Then run UIInspector on it: JPF finds the bug Replays it on the real UI for TestMe Collaborator Peter Mehlitz


Something Completely Different: Something Completely Different Well, maybe not completely… We developed a new static analysis tool for Java over the summer Aaron Tomb (USC) did all the hard work Problem we were addressing Static analyzers for finding defects are now popular tools, even commercial successes Coverity and KlockWork to name two But once they find a possible how do you know it is a real bug When we find a possible bug we want an input that will lead us to the bug Existing tools didn’t give us a hook into the internals to allow enough information to create such an input We developed a new tool based on symbolic execution to do it Hooked it into SOOT Used CVCLite as a decision procedure Once a constraint on the inputs is found that leads to a possible bug, we solve the constraints with POOC and run the code with those inputs Highly customizable Allows intra- or inter-procedural analysis Heuristics for finding array bounds exceptions Etc. Again work in progress, but has found real NASA bugs! Collaborator Aaron Tomb