The complete schedule is found on [http://learningsuite.byu.edu BYU Learning Suite]; though a tentative reading schedule is provided below for review. == Fall 2018 == Create a verification tool for a simple restricted language that is able to: * '''Static Check''' the program for type safety and that all variables are declared * '''Simulate''' the language prompting the user if ever there is a non-deterministic choice * '''Model Check''' simple linear temporal logic properties * '''Automatically generate tests''' for branch coverage * '''Abstract Interpret''' over simple abstractions for safety properties The language can use any syntax and minimally must support * Primitive types: char, int, and string (signed only) * Output to the console * Function calls with parameters, local variables, and single scope * Operators for integer linear arithmetic (plus, minus, and limited multiplication). * Standard relational operators: less-than, less-than-equal, equal, etc. * Logical operators: not, and, or * '''if-then-else''' statements * '''while''' statements * '''return''' statements * '''non-determistic input''' so that input can be defined over a range of values * '''Extra:''' a keyword to create threads of execution ===Parsing=== Please using any tool for the parsing. Write the grammar in whatever textural form is used by the tool being used to generate the parser. Here is an example of a [[Static Java]] language described for the ANTLR tool. It has a super set of the required language properties. If you are using an LL(n) parser then left-factoring and removing left recursion in the grammar will be important: * [http://www.csd.uwo.ca/~moreno/CS447/Lectures/Syntax.html/node9.html left-factoring] * [https://en.wikipedia.org/wiki/Left_recursion removing left recursion] The output of the parser should be an abstract syntax tree. Any language may be used to implement that tree (and the verification tool for that matter). It is highly recommended to use a [https://en.wikipedia.org/wiki/Visitor_pattern visitor pattern] with the abstract syntax tree. Note that one of the compiler passes will be to transform the language into [http://matt.might.net/articles/a-normalization/ A-normal form]. Here is the [https://en.wikipedia.org/wiki/A-normal_form Wiki version for A-normal Form]. You may define other passes to simplify simulation as desired. Here is a git repository with resources on ANTLR (see lectures/ANTLR-tutorial-calc git clone ssh://@schizo.cs.byu.edu/~egm/public-git/cs431/lectures There are also several lectures on the visitor pattern, symbol tables, and type checking. ===Static Check=== The tool should build a symbol table as a pass on the AST. That table should include functions and variables and ensure that only declared things or used. In a second pass, it should construct a type proof showing that all statements are type correct. ===Simulation=== Simulation is based on the [http://matt.might.net/articles/cesk-machines/ CESK framework]. A lighter read is [http://matt.might.net/articles/oo-cesk/ Java as a CESK machine]. A CESK machine defines state to consist of a control, environment, a store, and a continuation. It is a powerful model for semantics capable of handling all the complexity of higher-order languages. Although the language here is not high-order, the CESK model is a clean and convenient way to define the semantics of the language and give those semantics operational capabilities. Indeed, one of the strengths of CESK is that the semantic definition is operational. Semantics are defined by rules that govern transitions between states. Each rule defines the conditions that must hold in the source state with the conditions that must hold in the target state. The rules clearly define how the source state is related to the target state. ===Model Checking=== We are interested in model checking via automata theory. The basis is in language intersection where the model of the system forms one language and the property forms another language. The property is complemented and then the two languages, the model and complemented property, are intersected to see in there are any common words in the intersection. A word in the intersection is a counter example. There are two free online sources to study to learn the algorithms. The first is [http://is.ifmo.ru/books/_principles_of_model_checking.pdf Principles of Model Checking] Chapter 4. First study how to intersect NFAs, and then study sections 4.2 and 4.3 to apply it to infinite words on Buchi Automata. The infinite words capture liveness properties. The second online source is [https://mitpress.mit.edu/books/model-checking Model Checking] Chapter 9. This book is available, in electronic form, through the [http://library.byu.edu Harold B. Lee Library]. Click on ''Books'' on the left sidebar. Search for ''Model Checking'', and then follow the links to the electronic version. Here are the key topics that you need to understand: * Buchi automaton and infinite words * Intersecting Buchi automaton with the simplified algorithm where all states are accepting in one automaton * Double depth-first search for cycle detection * On-the-fly model checking * Converting a Kripke structure or labeled transition system to an automaton The project is to first introduce a key-word into the language, '''select (i : 1 .. N)''', for non-determinism. The meaning of the new key-word is to non-deterministically chooses a value for ''i'' from the range. Second, create an API to be able to hard-code a property automaton in the code, and then use it to intersect with the program under verification reporting the counter-example if one exists. ===Symbolic Execution for Source Code Verification=== Use symbolic execution to verify a use indicated function in the program. To support the verification, add to the language two statements: * '''assume''': takes a predicate on a variable and restricts that variable to ranges where the predicate is true. * '''assert''': takes a predicate on a variable and fails if that predicate is not true. With the addition of these two statements, it is possible to assume pre-conditions and assert post-conditions for program verification via symbolic execution. The symbolic execution for this assignment will use [https://people.eecs.berkeley.edu/~ksen/papers/multise.pdf path merging] to reduce the complexity of the search space. It will also require that the tool interface with an [http://smtlib.cs.uiowa.edu/ SMT solver]. There are several useful references for the needed background. Here are a few to get started: * [http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=1702368&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D1702368 A System to Generate Test Data and Symbolically Execute Programs] * [http://dl.acm.org/citation.cfm?id=360252 Symbolic execution and program testing] * [https://www.cs.upc.edu/~erodri/webpage/cps/lab/sat/tutorial-smt-solvers-slides/slides.pdf Tutorial on SMT Solvers] * [https://rise4fun.com/z3/tutorial Z3 - Guide] * [https://yurichev.com/writings/SAT_SMT_by_example.pdf SAT/SMT by Example] * [http://yices.csl.sri.com/papers/cav2007.pdf A Tutorial on Satisfiability Modulo Theories] * [https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf The SMT-LIBv2 Language and Tools: A Tutorial] * [http://homepages.inf.ed.ac.uk/pbj/papers/vct-dec09-draft.pdf Proving SPARK Verification Conditions with SMT Solvers]--very similar to this assignment The ultimate goal is to implement the [https://people.eecs.berkeley.edu/~ksen/papers/multise.pdf path merging] version of symbolic execution (the BDDs are a non-needed optimization) for your language, so read the background material enough to understand the approach. ===Abstract Interpretation=== == Fall 2017 == * [http://spinroot.com The SPIN Model Checker] (Eric Mercer) * [http://vsl.cis.udel.edu/civl/index.html Concurrency Intermediate Verification Language] * [http://valgrind.org/docs/manual/hg-manual.html Helgrind], , or [http://www.vi-hps.org/Tools/ARCHER.html ARCHER] * [https://github.com/rose-compiler/rose/tree/master/projects/CodeThorn CodeThorn] * (Stanley) [https://babelfish.arc.nasa.gov/trac/jpf Java Pathfinder] (do symbolic pathfinder too---SPF) * [https://github.com/ksen007/calfuzzer/blob/master/README.md CalFuzzer] * (Jeff) [http://psisolver.org/ PSI Probabilistic Program Solver] * (Jeff) Go-race detector with [https://clang.llvm.org/docs/ThreadSanitizer.html ThreadSanitizer] * (Jacob) [http://www.vprover.org/ Vampire: theorem proving for program analysis] * (Jeff) [http://www.prismmodelchecker.org/games/ PRISM-games: verification of collaborative behavior] * [http://www.cprover.org/cbmc/ CBMC: C bounded model checker] * (Jacob) [http://dl.acm.org/citation.cfm?id=3092704 One test to rule them all] * [https://xuanbachle.github.io/semanticsrepair/ JFix: semantics-based repaire for Java programs] * (Eric) [http://www-bcf.usc.edu/~wang626/pubDOC/GuoKW16.pdf Conc-iSE: incremental symbolic execution of Concurrent Software] * [https://github.com/ExpoSEJS/ExpoSE ExpoSE: DSE engine for JavaScript] * (Jacob) [https://bestchai.bitbucket.io/tsviz/ TSViz: visualization engine for complex multi-threaded systems], [https://dl.acm.org/citation.cfm?id=3098356 Studying multi-threaded behavior with TSViz] * (Vaishnavi) [https://users.soe.ucsc.edu/~cormac/papers/pldi17.pdf BigFoot Static Check Placement for Data Race] * (Stanley) [https://arxiv.org/abs/1704.02432 Dynamic Race Prediction in Linear Time] * (Vaishnavi) [http://dl.acm.org/citation.cfm?id=3062384 Flatten and conquer: a framework for efficient analysis of string constraints] * (Vaishnavi) [http://www.cse.unsw.edu.au/~tiantan/papers/pldi2017.pdf Efficient and Precise Points-to Analysis: Modeling the Heap by Merging Equivalent Automata] * [http://dl.acm.org/citation.cfm?id=3009857 Dynamic race detection for C++11] * (Stanley) [https://github.com/thomasjball/PyExZ3 PyEXZ3], Python based--Pycontracts, or model checking python code, or Python connectors to Z3 and NuSMV * Week 1: ** Overview ** Scheduling * Week 2: Symbolic Execution ** '''Canceled''' (no class) ** (Thursday -- Eric) [http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=1702368&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D1702368 A System to Generate Test Data and Symbolically Execute Programs] ** (Thursday -- Eric) [http://dl.acm.org/citation.cfm?id=360252 Symbolic execution and program testing] * Week 3: ** (Tuesday -- Eric) [http://www.cs.berkeley.edu/~ksen/papers/multise.pdf MultiSE: Multi-Path Symbolic Execution using Value Summaries] ** (Thursday -- Eric [https://arxiv.org/pdf/1610.00502.pdf A Survey of Symbolic Execution Techniques] * Week 4: ** (Tuesday -- Jacob) class time will cover vector clocks and prep output for TSViz *** Read [https://bestchai.bitbucket.io/tsviz/ TSViz: visualization engine for complex multi-threaded systems] *** Read [https://dl.acm.org/citation.cfm?id=3098356 Studying multi-threaded behavior with TSViz] *** Watch the video that is referenced in the paper *** Read the [https://bitbucket.org/mhnnunes/tsviz/wiki/LogFormat log format documentation] and the wikipedia description of [https://en.wikipedia.org/wiki/Vector_clock vector clocks], [http://basho.com/posts/technical/why-vector-clocks-are-hard/ Why vector clocks are hard], and a nice [https://www.youtube.com/watch?v=jD4ECsieFbE video demonstration] *** Write or find a meaningful threaded program and modify it to output the four required capture groups for TSViz ** (Thursday) -- '''Canceled - No class''' * Week 5: ** (Tuesday -- Jacob) [https://users.soe.ucsc.edu/~cormac/papers/popl05.pdf Dynamic Partial-Order Reduction for Model Checking Software] ** (Thursday -- Jacob) Same as Tuesday * Week 6: ** (Tuesday -- Jeff) [http://www.cs.columbia.edu/~junfeng/11fa-e6121/papers/thread-sanitizer.pdf ThreadSanitizer – data race detection in practice] ** (Thursday -- Jeff) [http://www.cs.columbia.edu/~junfeng/11fa-e6121/papers/thread-sanitizer.pdf ThreadSanitizer – data race detection in practice] * Week 7: ** (Tuesday -- Stanley) Install JPF in either Eclipse or Netbeans (or standalone command-line) and read the JPF Wiki: *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/start https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/start] *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/what_is_jpf https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/what_is_jpf] *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/testing_vs_model_checking https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/testing_vs_model_checking] *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/random_example https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/random_example] *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/race_example https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/race_example] *** [https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/classification https://babelfish.arc.nasa.gov/trac/jpf/wiki/intro/classification] ** (Thursday -- Stanley) [https://link.springer.com/content/pdf/10.1007%2Fs10515-013-0122-2.pdf Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis] * Week 8 ** (Tuesday -- Eric) [http://www-bcf.usc.edu/~wang626/pubDOC/GuoKW16.pdf Conc-iSE: incremental symbolic execution of Concurrent Software] ** (Thursday) [https://dl.acm.org/citation.cfm?id=2629536 Directed Incremental Symbolic Execution] * Week 9 ** (Tuesday) '''Canceled''' (no class) ** (Thursday -- Vaishnavi) [https://users.soe.ucsc.edu/~cormac/papers/pldi17.pdf BIGFOOT: Static Check Placement for Dynamic Race Detection] * Week 10 ** (Tuesday) Vaishnavi ** (Thursday -- Stanley) [https://arxiv.org/abs/1704.02432 Dynamic Race Prediction in Linear Time] * Week 11 ** (Tuesday -- Stanley) [https://arxiv.org/abs/1704.02432 Dynamic Race Prediction in Linear Time] ** (Thursday -- Jacob) [http://dl.acm.org/citation.cfm?id=3092704 One test to rule them all] * Week 12 '''No classes due to Thanksgiving Holiday''' * Week 13 ** (Tuesday -- Jacob) [http://dl.acm.org/citation.cfm?id=3092704 One test to rule them all] ** (Thursday -- Jacob) [http://dl.acm.org/citation.cfm?id=3092704 One test to rule them all] * Week 14 **(Tuesday) '''Canceled''' ''(illness)'' **(Thursday -- Vaishnavi) [http://dl.acm.org/citation.cfm?id=3062384 Flatten and conquer: a framework for efficient analysis of string constraints] * Week 14 ** (Tuesday -- Jeff) [https://spinroot.com/courses/summer/Papers/hoare_1978.pdf Communicating Sequential Processes] == Old Schedule == * Week 1: Introduction and Overview of Model Checking (language theoretic approach) ** Generate state space ** Convert to Buchi Automaton ** Write property automaton ** Language intersection: Tarjan's double depth-first search * Week 2: The SPIN Model Checker ** [https://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Principles of the SPIN Model Checker] * Week 2: Symbolic Execution ** [http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=1702368&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D1702368 A System to Generate Test Data and Symbolically Execute Programs] ** [http://dl.acm.org/citation.cfm?id=360252 Symbolic execution and program testing] * Week 3: Symbolic Execution for Strings ** [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4344094 Abstracting Symbolic Execution with String Analysis] ** [http://dl.acm.org/citation.cfm?id=2389853 Symbolic Execution of Programs with Strings] * Week 4: Symbolic Execution for Data-structures ** [http://babelfish.arc.nasa.gov/trac/jpf/ Java Path Finder (JPF)] ** [http://link.springer.com/article/10.1007/s10515-013-0122-2 Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis] ** [http://dl.acm.org/citation.cfm?id=2983940 JBSE: a symbolic executor for Java programs with Complex heap inputs] * Week 5: SAT Solving ** [https://en.wikipedia.org/wiki/Davis–Putnam_algorithm Davis-Putman Algorithm], [http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.pdf z3], and [https://utah.instructure.com/courses/348706/files/51060950/download?wrap=1 cs5959_lecture_09.pdf] ** [https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning Conflict-driven Clause Learning] and [https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf chaff] * Week 6: [http://www.cprover.org/cbmc/ CBMC]: C Bounded Model Checker ** [http://link.springer.com/chapter/10.1007%2F978-3-540-24730-2_15 A Tool for Checking ANSI-C Programs] ** (start on page 11) [http://reports-archive.adm.cs.cmu.edu/anon/2003/CMU-CS-03-126.pdf Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking] ** (reference if needed [http://fmv.jku.at/papers/BiereCimattiClarkeZhu-TACAS99.pdf Symbolic Model Checking without BDDs]) * Week 7: BMC with Concurrency ** [http://link.springer.com/chapter/10.1007%2F11513988_9 Bounded Model Checking of Concurrent Programs] ** [http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=5928354 SMT-Based Bounded Model Checking for Embedded ANSI-C Software] * Week 8: Stateless Model Checking with SAT ** [http://mir.cs.illinois.edu/marinov/publications/SenETAL05CUTE.pdf CUTE: A Concolic Unit Testing Engine for C] ** [http://plrg.eecs.uci.edu/publications/oopsla15mc.pdf SATCheck: SAT-directed stateless model checking for SC and TSO] * Week 9: IC3 ** [http://link.springer.com/chapter/10.1007/978-3-642-18275-4_7#page-1 SAT-Based Model Checking without Unrolling] (tutorial [http://theory.stanford.edu/~arbrad/papers/ic3_tut.pdf IC3: where monolithic and incremental meet]) ** [http://link.springer.com/chapter/10.1007/978-3-642-31424-7_23#page-1 Software Model Checking via IC3] * Week 10: State Merging ** [http://www.cs.berkeley.edu/~ksen/papers/multise.pdf MultiSE: Multi-Path Symbolic Execution using Value Summaries] ** [http://link.springer.com/chapter/10.1007/978-3-319-41528-4_21 Satisfiability Modulo Heap-based Programs] ** [http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_10 Exact Heap Summaries for Symbolic Execution] * Week 11: Testing Concurrent Programs ** [http://dl.acm.org/citation.cfm?id=2336779 Testing Concurrent Programs to Achieve High Synchronization Coverage] ** [http://web.eecs.umich.edu/~nsatish/papers/OOPSLA-12-Maple.pdf Maple: A Coverage-Driven Testing Tool for Multithreaded Programs] * Week 12: Regression Testing for Data-race ** [http://dl.acm.org/citation.cfm?id=2568294 SimRT: An Automated Framework to Support Regression Testing for Data Races] ** [http://dl.acm.org/citation.cfm?id=2818787 RECONTEST: Effective Regression Testing of Concurrent Programs] * Week 13: Incremental Testing ** [http://dl.acm.org/citation.cfm?id=1993558 Directed Incremental Symbolic Execution] ** [http://dl.acm.org/citation.cfm?id=2818817 A Flexible and Non-intrusive Approach for Computing Complex Structural Coverage Metrics.] * Week 14: Grab Bag ** [https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&ved=0ahUKEwijsLzIkc3KAhVJxWMKHftcBcYQFggtMAE&url=https%3A%2F%2Fwww.nicta.com.au%2Fpub-download%2Fslides%2F8582%2F&usg=AFQjCNFi03S6hb_5biy0IOroG0EnSPYnCQ From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis] ** [https://www.cs.purdue.edu/homes/suresh/papers/cav15.pdf Poling: SMT Aided Linearizability Proofs] ** [https://www.cs.utah.edu/~regehr/papers/pldi15.pdf Provably Correct Peephole Optimizations with Alive] ** [https://parasol.tamu.edu/~jeff/academic/mcr.pdf Stateless Model Checking Concurrent Programs with Maximal Causality Reduction] ** [http://delivery.acm.org/10.1145/2740000/2737998/p175-samak.pdf?ip=128.187.97.25&id=2737998&acc=ACTIVE%20SERVICE&key=B63ACEF81C6334F5%2EE4A70A1B77145BCF%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35&CFID=578672705&CFTOKEN=16838057&__acm__=1454006718_09b298c93eb468058312b9214a4160ce Synthesizing racy tests] ** [http://dl.acm.org/citation.cfm?id=2737973 Concurrency Debugging with Differential Schedule Projections] ** [http://dl.acm.org/citation.cfm?id=2737966 Automated Detection of Performance Bugs via Static Analysis] ** [https://www.cis.upenn.edu/~alur/Pldi07.pdf CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models] * Week 15 Verification Reports * Use one of the studied tools or techniques to verify a piece of software written for your research or a class project. Report your experience. == Tools To Consider == * [http://babelfish.arc.nasa.gov/trac/jpf/ Java Path Finder (JPF)] * [http://klee.llvm.org/ The KLEE Symbolic Virtual Machine] * [http://pex4fun.com/ Pex] * [http://www.cprover.org/cbmc/ CBMC] * [http://www.cprover.org/wolverine/ Wolverine] (lazy abstraction with interpolants) * [http://mtc.epfl.ch/software-tools/blast/index-epfl.php BLAST: Berkeley Lazy Abstraction Software Verification Tool] * [http://research.microsoft.com/en-us/projects/slayer/ Slayer] * [http://findbugs.sourceforge.net/ Findbugs - Find bugs in Java programs] * [http://kindsoftware.com/products/opensource/ESCJava2/ ESC/Java 2] * [http://spinroot.com/spin/whatispin.html The SPIN Model Checker] ** [http://spinroot.com/spin/Man/ SPIN Online Manual] * [http://www.cs.utah.edu/formal_verification/ISP-Release/ ISP (In-situ Partial Order): a dynamic verifier for MPI Programs] (dynamic partial order reduction) ** [http://link.springer.com/chapter/10.1007%2F978-3-540-70545-1_9 Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings] ** Secondary paper of possible interest: [http://www.cs.utah.edu/formal_verification/pdf/sbmf_2012.pdf A Sound Reduction of Persistent-sets for Deadlock Detection in MPI Applications] *[http://klee.llvm.org/ The KLEE Symbolic Virtual Machine] ** [https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar_html/ KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs] * [http://srl.cs.berkeley.edu/~ksen/calfuzzer/ CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs] ** [http://dl.acm.org/citation.cfm?id=1542489 A randomized dynamic program analysis technique for detecting real deadlocks] * Counter Example Guided Abstraction Refinement ** [http://dl.acm.org/citation.cfm?doid=378795.378846 Automatic Predication Abstraction of C programs] ** [http://delivery.acm.org/10.1145/510000/503274/p1-ball.pdf?ip=128.187.80.2&id=503274&acc=ACTIVE%20SERVICE&key=C2716FEBFA981EF18F50507BD85933485DE900CB1EEBF499&CFID=233624694&CFTOKEN=46108260&__acm__=1373927757_366bc75fbabffdaa12a892f3419c31ce The SLAM Project: Debugging System Software via Static Analysis] * [http://www.cprover.org/wolverine/ Wolverine] (lazy abstraction with interpolants) ** [http://www.cprover.org/wolverine/download/cav11.pdf Interpolation-based Software Verification with Wolverine] (see for reference [http://dl.acm.org/citation.cfm?id=503279 Lazy Abstraction]) * [http://findbugs.sourceforge.net/ Findbugs - Find bugs in Java programs] ** [http://dl.acm.org/citation.cfm?id=2486877 Why don't software developers use static analysis tools to find bugs?] ** [http://findbugs.cs.umd.edu/papers/MoreNullPointerBugs07.pdf Finding More Null Pointer Bugs, But Not Too Many] * [http://kindsoftware.com/products/opensource/ESCJava2/ ESC/Java 2] ** [http://dl.acm.org/citation.cfm?id=512558 Extended Static Checking for Java] ** [http://dl.acm.org/citation.cfm?id=360220 Avoiding exponential explosion: generating compact verification conditions] * Type Systems ** [http://dl.acm.org/citation.cfm?id=2254094 Fast and precise hybrid type inference for JavaScript] == Papers for another day == * [http://dl.acm.org/citation.cfm?id=2032360 Practical, low-effort equivalence verification of real code] * [http://dl.acm.org/citation.cfm?id=2254088 Efficient State Merging in Symbolic Execution] * [http://dl.acm.org/citation.cfm?id=1081750 CUTE: a concolic unit testing engine for C] * [http://link.springer.com/chapter/10.1007%2F978-3-642-31057-7_27 Practical Permissions for Race-free Parallelism] * [http://link.springer.com/chapter/10.1007%2F978-3-642-03351-3_4 Automatic Verification of Heap-Manipulating Programs Using Separation Logic] * [http://link.springer.com/article/10.1007%2Fs10703-005-1489-x Software Model Checking: The Verisoft Approach] * [http://dl.acm.org/citation.cfm?id=1998508SLAM2: Static Driver Verification with Under 4% False Alarms] * [http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Checker_BLAST.pdf The Software Model Checker BLAST] * [http://dl.acm.org/citation.cfm?id=1941509 Proving program termination] * [http://www0.cs.ucl.ac.uk/staff/b.cook/cav11b.pdf SLAYER: Memory Safety for Systems-level Code] * [http://dl.acm.org/citation.cfm?id=1065036 DART: directed automated random testing] * [http://dl.acm.org/citation.cfm?id=2094081 SAGE: Whitebox Fuzzing for Security Testing] * [http://dl.acm.org/citation.cfm?id=1040315 Dynamic partial-order reduction for model checking software] * [http://dl.acm.org/citation.cfm?id=1765871.1765924 Generalized symbolic execution for model checking and testing]\ * [http://research.microsoft.com/pubs/141925/popl198ap-emmi.pdf Delay-Bounded Scheduling]