We extend the scope of context-free-language (CFL) reachability to a new class of infinite-state systems. Parikh's Theorem is a useful tool for solving CFL-reachability problems for transition systems that consist of commuting transition relations. It implies that the image of a context-free language under a homomorphism into a commutative monoid is semi-linear, and that there is a linear-time algorithm for constructing a Presburger arithmetic formula that represents it. However, for many transition systems of interest, transitions do not commute. In this paper, we introduce almost-commuting transition systems , which pair finite-state control with commutative components, but which are in general not commutative. We extend Parikh's theorem to show that the image of a context-free language under a homomorphism into an almost-commuting monoid is semi-linear and that there is a polynomial-time algorithm for constructing a Presburger arithmetic formula that represents it. This result yields a general framework for solving CFL-reachability problems over almost commuting transition systems . We describe several examples of systems within this class. Finally, we examine closure properties of almost-commuting monoids that can be used to modularly compose almost-commuting transition systems while remaining in the class.

Memory safety is an important property for security-critical systems, but it cannot be easily extended to cryptography, which is a common source of memory safety vulnerabilities. Cryptography libraries use assembly for direct control of timing and performance, but assembly introduces unsafety when it is called from a high-level memory-safe language like Rust. To enable quick and safe integration of assembly into Rust, specifically for building memory-safe cryptography, we present CLAMS. CLAMS verifies cryptographic assembly against safety constraints derived directly from Rust's type system. Verification is done through symbolic execution at compile time to minimize run-time overheads, and supports verifying loops over potentially unbounded input buffers. CLAMS's procedural macro interface forces developers to map safe Rust types to registers and define preconditions on input and output parameters. CLAMS's techniques can verify the memory safety of assembly from a popular open-source cryptography library. We evaluated CLAMS and found that verification is quick and imposes compile-time overheads under 100ms and negligible run-time overheads.

This paper presents a technique for summarizing recursive procedures operating on integer variables. The motivation of our work is to create more predictable program analyzers, and in particular to formally guarantee compositionality and monotonicity of procedure summarization. To summarize a procedure, we compute its best abstraction as a vector addition system with resets (VASR) and exactly summarize the executions of this VASR over the context-free language of syntactic paths through the procedure. We improve upon this technique by refining the language of syntactic paths using (automatically synthesized) linear potential functions that bound the number of recursive calls within valid executions of the input program. We implemented our summarization technique in an automated program verification tool; our experimental evaluation demonstrates that our technique computes more precise summaries than existing abstract interpreters and that our tool’s verification capabilities are comparable with state-of-the-art software model checkers.

We describe an online approach to SMT solver selection using nearest neighbor classification and runtime estimation. We implement and evaluate our approach with MedleySolver, finding that it makes nearly optimal selections and evaluates a dataset of queries three times faster than any indivdual solver.