20 citations · 34 across the 10 of their papers we have counts for
12 papers
Inductive Predicate Synthesis Modulo Programs (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the…
DesCert: Design for Certification
Natarajan Shankar, Devesh Bhatt, Michael Ernst +8
The goal of the DARPA Automated Rapid Certification Of Software (ARCOS) program is to "automate the evaluation of software assurance evidence to enable certifiers to determine rapi…
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existin…
Automatically Tailoring Static Analysis to Custom Usage Scenarios
Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis +2
In recent years, there has been significant progress in the development and industrial adoption of static analyzers. Such analyzers typically provide a large, if not huge, number o…
Unification-based Pointer Analysis without Oversharing
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyse…
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
Graeme Gange, Jorge A. Navas, Peter Schachte +2
Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propo…