We present mechanisms to specify and efficiently check, at runtime, assertions that express structural properties and aggregate measures of dynamically manipulated linkedlist data structures. Checking assertions involving the structure, disjointness, and aggregation measures on lists and list segments typically requires linear or quadratic time in the size of the heap. Our main contribution is an incrementalization instrumentation that tracks properties of data structures dynamically as the program executes and leads to orders of magnitude speedup in assertion checking in many scenarios. Our incrementalization incurs a constant overhead on updates to list structures but enables checking assertions in constant time, independent of the size of the heap. We define a general class of functions on lists, called linear measures, which are amenable to our incrementalization technique. We demonstrate the effectiveness of our technique by showing orders of magnitude speedup in two scenarios: one scenario stemming from assertions at the level of APIs of list-manipulating libraries and the other scenario stemming from providing dynamic detection of security attacks caused by malicious rootkits.

The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32].

Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our use of formal methods for proving key security invariants about our implementation. In our use of formal methods, we focus solely on proving that our OS implements our security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of our system.

Theory propagation in Satisfiability Modulo Theories is crucial for the solver's performance. It is important, however, to pay particular care to the amount of deductions to perform. The risk is in fact to clog the SAT-Solver with too many (and potentially useless clauses). In this paper we review some techniques for generating and communicating clauses to the SAT-Solver. In addition we propose a generic and flexible schema for theory propagation in which explanations for entailed facts are generated by re-using the consistency check procedure that is normally available in a theory solver. We argue that our schema can simplify the design of a theory solver, and allow a flexible form of theory propagation even for inherently hard theories (such as bit-vectors).