Home | Research | Music | Photography | Software | Blog

Research

Invariant Generation for Container-manipulating Programs

This work automatically infers relational invariants between sets in a set-manipulating program. We use these sets to abstract the key sets of dictionaries in objects in Python and JavaScript. I developed a tool that uses an innovative data structure called a QUIC graph to capture relations between sets and external variables and values.

More information and the tool and source is available on the project page.

Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan. QUIC Graphs: Relational Invariant Generation for Containers. ECOOP 2013. Paper PDF

Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan. QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. CAV 2014. Paper PDF

Diagnosing Abstraction Failure for Separation Logic-Based Analyses

While on an internship at Microsoft Research, Cambridge, I worked with Samin Ishtiaq, Josh Berdine and Christoph Wintersteiger to develop a method for finding counterexamples for separation logic-based analyses performed by the SLAyer tool. The method involved encoding the transition system produced by SLAyer into a SMT formula and querying it for a set of inputs that would lead a program to error.

I developed a memory model, inspired by the model that SLAyer and other C analysis tools use, translated that into SMT using the new quantified bit-vectors theory provided by Z3. Using the counterexamples produced by this tool, we developed a technique to use forward-only analysis to perform simple refinements. This provided us with efficiency that was never before possible.

Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph Wintersteiger. Diagnosing Abstraction Failure in Separation Logic-based Analyses. CAV 2012. Paper PDF Talk PDF, Talk PPTX

Arlen Cox, Samin Ishtiaq, Josh Berdine, Christoph Wintersteiger. Counterexample Generation for Separation-Logic-based Proofs. Z3 SIG 2011. Talk PPTX

Bit-precise Bug Finding in Digital Filters

Recently I developed a method and tool for finding bugs in fixed- point implementations of digital filters. The tool uses model-checking and word-level modelling to quickly verify finite- impulse-response and find bugs in infinite-impulse-response filters. The tool also implements a simulator, real-based error approximations and affine approximations.

Update: Documentation is now available for input format. Filters can be more easily reused by other tools.

The software is available for download.

Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang. A bit too precise? Verification of digital filters. STTT 2013. Paper PDF

Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang. A Bit Too Precise? Bounded Verification of Digital Filters. TACAS 2012. Paper PDF Talk PDF, Talk Keynote

CNF Conversion for Model Checking

My previous research project right was understanding the consequences of different CNF conversions on different model checking engines. Prior work has shown that SAT can be greatly affected by the CNF conversion, but there does not appear to be a direct correlation between SAT performance and model checking performance. Therefore it is important to classify the different types of problems that are benefited by different solving approaches used by different SAT solvers.

The original version of IC3 used a primitive version of technology mapping for CNF conversion that was based on the paper by Eén, Mishchenko and Sörensson. While this did give IC3 an additional solve or two, further study has shown that it is not universally beneficial. Therefore I am looking at the current CNF conversion approaches by the ABC group, the BAT group and comparing them to the traditional Tseitin approach used by aigcnf and many other tools.

The CNF converters are implemented as part of the IIMC project. They are closely integrated with the model checking engines and are tuned for performance. The CNF conversion operates on the transition relation that is used for both IC3-based and BMC-based analysis.

With the departure of my previous advisor, Dr. Aaron Bradley, This work has been terminated. A tech report will be produced to summarize the work. There were problems with our reimplementation of the NiceDAGs- based CNF conversion that prevented its publication

Program Analysis of Business Logic

Business logic is one of the most prevalent styles of code in use in the world today. A large percentage of this is written in the COBOL programming languages. In cooperation with ioSemantics, I am developing a context-sensitive program analysis system that will be used to rapidly explore COBOL code.

A context-sensitive analysis, as opposed to a path-sensitive analysis, considers all possible entry conditions to functions individually. A path sensitive analysis might consider all the states in which a function can be entered. Using this as the precondition for a function, it will compute the post-image of the function and use that everywhere the function is called. In the context-sensitive analysis, it will consider each condition under which the function can be called individually.

Home | Research | Music | Photography | Software | Blog