Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017.

The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.



Bringing LTL Model Checking to Biologists

The BioModelAnalyzer (BMA) is a web based tool for the development of discrete models of biological systems. Through a graphical user interface, it allows rapid development of complex models of gene and protein interaction networks and stability analysis without requiring users to be proficient computer programmers. Whilst stability is a useful specification for testing many systems, testing temporal specifications in BMA presently requires the user to perform simulations. Here we describe the LTL module, which includes a graphical and natural language interfaces to testing LTL queries. The graphical interface allows for graphical construction of the queries and presents results visually in keeping with the current style of BMA. The Natural language interface complements the graphical interface by allowing a gentler introduction to formal logic and exposing educational resources.
Zara Ahmed, David Benque, Sergey Berezin, Anna Caroline E. Dahl, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Jay Nanavati, Nir Piterman, Maik Riechert, Nikita Skoblov

Detecting Strict Aliasing Violations in the Wild

Type-based alias analyses allow C compilers to infer that memory locations of distinct types do not alias. Idiomatic reliance on pointers on the one hand, and separate compilation on the other hand, together make it impossible to get this aliasing information any other way. As a consequence, most modern optimizing C compilers implement some sort of type-based alias analysis. Unfortunately, pointer conversions, another pervasive idiom to achieve code reuse in C, can interact badly with type-based alias analyses. This article investigate the fine line between the allowable uses of low-level constructs (pointer conversions, unions) that should never cause the predictions of a standard-compliant type-based alias analysis to be wrong, and the dangerous uses that can result in bugs in the generated binary. A sound and precise analyzer for “strict aliasing” violations is briefly described.
Pascal Cuoq, Loïc Runarvot, Alexander Cherepanov

Effective Bug Finding in C Programs with Shape and Effect Abstractions

Software tends to suffer from simple resource mis-manipulation bugs, such as double-locks. Code scanners are used extensively to remove these bugs from projects like the Linux kernel. Yet, these tools are not effective when the manipulation of resources spans multiple functions. We present a shape-and-effect analysis for C, that enables efficient and scalable inter-procedural reasoning about resource manipulation. This analysis builds a program abstraction based on the observable side-effects of functions. Bugs are found by model checking this abstraction, matching undesirable sequences of operations. We implement this approach in the Eba tool, and evaluate it on a collection of historical double-lock bugs from the Linux kernel. Our results show that our tool is more effective at finding bugs than similar code-scanning tools. Eba analyzes nine thousand Linux files in less than half an hour, and uncovers double-lock bugs in various drivers.
Iago Abal, Claus Brabrand, Andrzej Wąsowski

Synthesizing Non-Vacuous Systems

Vacuity detection is a common practice accompanying model checking of hardware designs. Roughly speaking, a system satisfies a specification vacuously if it can satisfy a stronger specification obtained by replacing some of its subformulas with stronger expressions. If this happens then part of the specification is immaterial, which typically indicates that there is a problem in the model or the specification itself.
We propose to apply the concept of vacuity to the synthesis problem. In synthesis, there is often a problem that the specifications are incomplete, hence under-specifying the desired behaviour, which may lead to a situation in which the synthesised system is different than the one intended by the designer. To address this problem we suggest an algorithm and a tool for non-vacuous bounded synthesis. It combines synthesis for universal and existential properties; the latter stems from the requirement to have at least one interesting witness for each strengthening of the specification. Even when the system satisfies the specification non-vacuously, our tool is capable of improving it by synthesizing a system that has additional interesting witnesses. The user decides when the system reflects their intent.
Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Static Analysis of Communicating Processes Using Symbolic Transducers

We present a general model allowing static analysis based on abstract interpretation for systems of communicating processes. Our technique, inspired by Regular Model Checking, represents set of program states as lattice automata and programs semantics as symbolic transducers. This model can express dynamic creation/destruction of processes and communications. Using the abstract interpretation framework, we are able to provide a sound over-approximation of the reachability set of the system thus allowing us to prove safety properties. We implemented this method in a prototype that targets the MPI library for C programs.
Vincent Botbol, Emmanuel Chailloux, Tristan Le Gall

Reduction of Workflow Nets for Generalised Soundness Verification

This paper proposes a reduction method to verify the generalised soundness of large workflows described as workflow nets–a suited class of Petri nets. The proposed static analysis method is based on the application of six novel reduction transformations that transform a workflow net into a smaller one while preserving generalised soundness. The soundness of the method is proved. As practical contributions, this paper presents convincing experimental results obtained using a dedicated tool, developed to validate and demonstrate the effectiveness, efficiency and scalability of this method over a large set of industrial workflow nets.
Hadrien Bride, Olga Kouchnarenko, Fabien Peureux

Structuring Abstract Interpreters Through State and Value Abstractions

We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design \({\textsc {eva}}\), an abstract interpreter for C implemented within the \(\textsc {Frama}\text {-}\textsc {C}\) framework. We present the domains that are available so far within \({\textsc {eva}}\), and show that this communication mechanism is able to handle them seamlessly.
Sandrine Blazy, David Bühler, Boris Yakobowski

Matching Multiplications in Bit-Vector Formulas

Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula. We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula that encode the equivalence of sub-terms and word-level multiplication terms. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.
Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

Independence Abstractions and Models of Concurrency

Mathematical representations of concurrent systems rely on two fundamental notions: an atomic unit of behaviour called an event, and a constraint called independence which asserts that the order in which certain events occur does not affect the final configuration of the system. We apply abstract interpretation to study models of concurrency by treating events and independence as abstractions. Events arise as Boolean abstractions of traces. Independence is a parameter to an abstraction that adds certain permutations to a set of sequences of events. Our main result is that several models of concurrent system are a composition of an event abstraction and an independence specification. These models include Mazurkiewicz traces, pomsets, prime event structures, and transition systems with independence. These results establish the first connections between abstraction interpretation and event-based models of concurrency and show that there is a precise sense in which independence is a form of abstraction.
Vijay D’Silva, Daniel Kroening, Marcelo Sousa

Complete Abstractions and Subclassical Modal Logics

Forwards-completeness is a concept in abstract interpretation expressing that an abstract and a concrete transformer have the same semantics with respect to an abstraction. When the set of transformers is generated by the signature of a logic, a forwards-complete abstraction of a structure is one that satisfies the same formulae in a given logic. We highlight a connection between models of positive modal logic, which are logics that lack negation and implication, and forwards-completeness. These models, which were discovered independently by researchers in modal logic, model checking, and static analysis of logic programs, correspond to Kripke structures with an order on their states. We show that forwards-completeness provides a new way to synthesize both models for positive modal logics and a notion of simulation for these models. The Kripke structures that can be synthesized using forwards-completeness satisfy a saturation condition which ensures that transition relations behave like best abstract transformers.
Vijay D’Silva, Marcelo Sousa

Using Abstract Interpretation to Correct Synchronization Faults

We describe a novel use of abstract interpretation in which the abstract domain informs a runtime system to correct synchronization failures. To this end, we first introduce a novel synchronization paradigm, dubbed corrective synchronization, that is a generalization of existing approaches to ensuring serializability. Specifically, the correctness of multi-threaded execution need not be enforced by previous methods that either reduce parallelism (pessimistic) or roll back illegal thread interleavings (optimistic); instead inadmissible states can be altered into admissible ones. In this way, the effects of inadmissible interleavings can be compensated for by modifying the program state as a transaction completes, while accounting for the behavior of concurrent transactions. We have proved that corrective synchronization is serializable and give conditions under which progress is ensured. Next, we describe an abstract interpretation that is able to compute these valid serializable post-states w.r.t. a transaction’s entry state by computing an under-approximation of the serializable intermediate (or final) states as the fixpoint solution over an inter-procedural control-flow graph. These abstract states inform a runtime system that is able to perform state correction dynamically. We have instantiated this setup to clients of a Java-like Concurrent Map data structure to ensure safe composition of map operations. Finally, we report early encouraging results that the approach competes with or out-performs previous pessimistic or optimistic approaches.
Pietro Ferrara, Omer Tripp, Peng Liu, Eric Koskinen

Property Directed Reachability for Proving Absence of Concurrent Modification Errors

We define and implement an interprocedural analysis for automatically checking safety of recursive programs with an unbounded state space. The main idea is to infer modular universally quantified inductive invariants in the form of procedure summaries that are sufficient to prove the safety property. We assume that the effect of the atomic commands of the program can be modeled via effectively propositional logic. We then propose a variant of the IC3/PDR approach for computing universally quantified inductive procedure summaries that overapproximate the behavior of the program.
We show that Java programs that manipulate collections and iterators can be modeled in effectively propositional logic and that the invariants are often universal. This allows us to apply the new analysis to prove the absence of concurrent modification exceptions in Java programs. In order to check the feasibility of our method, we implemented our analysis on top of Z3, as well as a Java front-end which translates Java programs into effectively propositional formulas.
Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham

Stabilizing Floating-Point Programs Using Provenance Analysis

Floating-point arithmetic is a loosely standardized approximation of real arithmetic available on many computers today. Architectural and compiler differences can lead to diverse calculations across platforms, for the same input. If left untreated, platform dependence, called volatility in this paper, seriously interferes with result reproducibility and, ultimately, program portability. We present an approach to stabilizing floating-point programs against volatility. Our approach, dubbed provenance analysis, traces volatility observed in a given intermediate expression E back to volatility in preceding statements, and quantifies individual contributions to the volatility in E. Statements contributing the most are then stabilized, by disambiguating the arithmetic using expression rewriting and control pragmas. The benefit of local (as opposed to program-wide) stabilization is that compilers are free to engage performance- or precision-enhancing optimizations across program fragments that do not destabilize E. We have implemented our technique in a dynamic analysis tool that reports both volatility and provenance information. We demonstrate that local program stabilization often suffices to reduce platform dependence to an acceptable level.
Yijia Gu, Thomas Wahl

Dynamic Reductions for Model Checking Concurrent Software

Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we accommodate dynamic transactions, and thereby reduce dependence on the accuracy of static analysis, which is a severe bottleneck in other reduction techniques.
The combination of symbolic model checking and dynamic reduction techniques has proven to be challenging in the past. Our generic reduction theorem nonetheless enables us to derive an efficient symbolic encoding, which we implemented for IC3 and BMC. The experiments demonstrate the power of dynamic reduction on several case studies and a large set of SVCOMP benchmarks.
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that—in contrast to existing techniques—tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states.
Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

In the context of shape analysis, counterexample validation and abstraction refinement are complex and so far not sufficiently resolved problems. We provide a novel solution to both of these problems in the context of fully-automated and rather general shape analysis based on forest automata. Our approach is based on backward symbolic execution on forest automata, allowing one to derive automata-based interpolants and refine the automata abstraction used. The approach allows one to distinguish true and spurious counterexamples and guarantees progress of the abstraction refinement. We have implemented the approach in the Forester tool and present promising experimental results.
Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Tomáš Vojnar

Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT

Statement-wise abstract interpretation that calculates the abstract semantics of a program statement by statement, is scalable but may cause precision loss due to limited local information attached to each statement. While Satisfiability Modulo Theories (SMT) can be used to characterize precisely the semantics of a loop-free program fragment, it is challenging to analyze loops efficiently using plainly SMT formula. In this paper, we propose a block-wise abstract interpretation framework to analyze a program block by block via combining abstract domains with SMT. We first partition a program into blocks, encode the transfer semantics of a block through SMT formula, and at the exit of a block we abstract the SMT formula that encodes the post-state of a block w.r.t. a given pre-state into an abstract element in a chosen abstract domain. We leverage the widening operator of abstract domains to deal with loops. Then, we design a disjunctive lifting functor on top of abstract domains to represent and transmit useful disjunctive information between blocks. Furthermore, we consider sparsity inside a large block to improve efficiency of the analysis. We develop a prototype based on block-wise abstract interpretation. We have conducted experiments on the benchmarks from SV-COMP 2015. Experimental results show that block-wise analysis can check about 1x more properties than statement-wise analysis does.
Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang

Solving Nonlinear Integer Arithmetic with MCSAT

We present a new method for solving nonlinear integer arithmetic constraints. The method relies on the MCSat approach to solving nonlinear constraints, while using branch and bound in a conflict-directed manner. We report encouraging experimental results where the new procedure outperforms state-of-the-art SMT solvers based on bit-blasting.
Dejan Jovanović

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

Fault-tolerant distributed algorithms are a vital part of mission-critical distributed systems. In principle, automatic verification can be used to ensure the absence of bugs in such algorithms. In practice however, model checking tools will only establish the correctness of distributed algorithms if message passing is encoded efficiently. In this paper, we consider abstractions suitable for many fault-tolerant distributed algorithms that count messages for comparison against thresholds, e.g., the size of a majority of processes. Our experience shows that storing only the numbers of sent and received messages in the global state is more efficient than explicitly modeling message buffers or sets of messages. Storing only the numbers is called message-counting abstraction. Intuitively, this abstraction should maintain all necessary information. In this paper, we confirm this intuition for asynchronous systems by showing that the abstract system is bisimilar to the concrete system. Surprisingly, if there are real-time constraints on message delivery (as assumed in fault-tolerant clock synchronization algorithms), then there exist neither timed bisimulation, nor time-abstracting bisimulation. Still, we prove this abstraction useful for model checking: it preserves ATCTL properties, as the abstract and the concrete models simulate each other.
Igor Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi

Efficient Elimination of Redundancies in Polyhedra by Raytracing

A polyhedron can be represented as constraints, generators or both in the double description framework. Whatever the representation, most polyhedral operators spend a significant amount of time to maintain minimal representations. To minimize a polyhedron in constraints-only representation, the redundancy of each constraint must be checked with respect to others by solving a linear programming (lp) problem. We present an algorithm that replaces most lp problem resolutions by distance computations. It consists in launching rays starting from a point within the polyhedron and orthogonal to its bounding hyperplanes. A face first encountered by one of these rays is an irredundant constraint of the polyhedron. Since this procedure is incomplete, lp problem resolutions are required for the remaining undetermined constraints. Experiments show that our algorithm drastically reduces the number of calls to the simplex, resulting in a considerable speed improvement. To follow the geometric interpretation, the algorithm is explained in terms of constraints but it can also be used to minimize generators.
Alexandre Maréchal, Michaël Périn

Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions

We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments and comparison with ConcurInterproc show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.
Raphaël Monat, Antoine Miné

Detecting All High-Level Dataraces in an RTOS Kernel

A high-level race occurs when an execution interleaves instructions corresponding to user-annotated critical accesses to shared memory structures. Such races are good indicators of atomicity violations. We propose a technique for detecting all high-level dataraces in a system library like the kernel API of a real-time operating system (RTOS) that relies on flag-based scheduling and synchronization. Our methodology is based on model-checking, but relies on a meta-argument to bound the number of task processes needed to orchestrate a race. We describe our approach in the context of FreeRTOS, a popular RTOS in the embedded domain.
Suvam Mukherjee, Arun Kumar, Deepak D’Souza

Reachability for Dynamic Parametric Processes

In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.
Anca Muscholl, Helmut Seidl, Igor Walukiewicz

Conjunctive Abstract Interpretation Using Paramodulation

Scaling static analysis is one of the main challenges for program verification in general and for abstract interpretation in particular. One way to compactly represent a set of states is using a formula in conjunctive normal form (CNF). This can sometimes save exponential factors. Therefore, CNF formulae are commonly used in manual program verification and symbolic reasoning. However, it is not used in abstract interpretation, due to the complexity of reasoning about the effect of program statements when the states are represented this way.
We present algorithms for performing abstract interpretation on CNF formulae recording equality and inequalities of ground terms. Here, terms correspond to the values of variables and of addresses and contents of dynamically allocated memory locations, and thus, a formula can represent pointer equalities and inequalities. The main idea is the use of the rules of paramodulation as a basis for an algorithm that computes logical consequences of CNF formulae, and the application of the algorithm to perform joins and transformers.
The algorithm was implemented and used for reasoning about low level programs. We also show that our technique can be used to implement best transformers for a variant of Connection Analysis via a non-standard interpretation of equality.
Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

Separation Logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schönfinkel-Ramsey quantifier prefix \(\exists ^*\forall ^*\), where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment [7]. However, \(\mathsf {SL}\) becomes undecidable when the quantifier prefix belongs to \(\exists ^*\forall ^*\exists ^*\) instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within \(\mathsf {SL}\). We have implemented a decision procedure for the decidable fragment of \(\exists ^*\forall ^*\mathsf {SL}\) as a specialized solver inside a DPLL(T) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.
Andrew Reynolds, Radu Iosif, Cristina Serban

Finding Relevant Templates via the Principal Component Analysis

The polyhedral model is widely used for the static analysis of programs, thanks to its expressiveness but it is also time consuming. To cope with this problem, weak-polyhedral analysis have been developed which offer a good trade off between expressiveness and efficiency. Some of these analysis are based on templates which fixed the form of the program’s invariant. These templates are defined statically at the beginning of the analysis, without taking into account the dynamic of programs. Finding good templates is a difficult problem. In this article, we present a method that uses the Principal Component analysis to compute an interesting template. We demonstrate the relevancy of the obtained templates on several benchmarks.
Yassamine Seladji

Sound Bit-Precise Numerical Domains

This paper tackles the challenge of creating a numerical abstract domain that can identify affine-inequality invariants while handling overflow in arithmetic operations over bit-vector data-types. The paper describes the design and implementation of a class of new abstract domains, called the Bit-Vector-Sound, Finite-Disjunctive (\(\textit{BVSFD}\)) domains. We introduce a framework that takes an abstract domain \(\mathcal {A}\) that is sound with respect to mathematical integers and creates an abstract domain \(\textit{BVS}(\mathcal {A})\) whose operations and abstract transformers are sound with respect to machine integers. We also describe how to create abstract transformers for \(\textit{BVS}(\mathcal {A})\) that are sound with respect to machine arithmetic. The abstract transformers make use of an operation \(\textit{WRAP}(\textit{av}, v)\)—where \(\textit{av} \in \mathcal {A}\) and v is a set of program variables—which performs wraparound in av for the variables in v.
To reduce the loss of precision from \(\textit{WRAP}\), we use finite disjunctions of \(\textit{BVS}(\mathcal {A})\) values. The constructor of finite-disjunctive domains, \(\textit{FD}_k(\cdot )\), is parameterized by k, the maximum number of disjunctions allowed.
We instantiate the \(\textit{BVS}(\textit{FD}_k)\) framework using the abstract domain of polyhedra and octagons. Our experiments show that the analysis can prove \(25\%\) of the assertions in the SVCOMP loop benchmarks with \(k=6\), and \(88\%\) of the array-bounds checks in the SVCOMP array benchmarks with \(k=4\).
Tushar Sharma, Thomas Reps

IC3 - Flipping the E in ICE

Induction is a key element of state-of-the-art verification techniques. Automatically synthesizing and verifying inductive invariants is at the heart of Model Checking of safety properties. In this paper, we study the relationship between two popular approaches to synthesizing inductive invariants: SAT-based Model Checking (SAT-MC) and Machine Learning-based Invariant Synthesis (MLIS). Our goal is to identify and formulate the theoretical similarities and differences between the two frameworks. We focus on two flagship algorithms: IC3 (an instance of SAT-MC) and ICE (an instance of MLIS). We show that the two frameworks are very similar yet distinct. For a meaningful comparison, we introduce RICE, an extension of ICE with relative induction and show how IC3 can be implemented as an instance of RICE. We believe this work contributes to the understanding of inductive invariant synthesis and will serve as a foundation for further improvements to both SAT-MC and MLIS algorithms.
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik

Partitioned Memory Models for Program Analysis

Scalability is a key challenge in static analysis. For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. In this paper, we explore a family of memory models called partitioned memory models which divide memory up based on the results of a points-to analysis. We review Steensgaard’s original and field-sensitive points-to analyses as well as Data Structure Analysis (DSA), and introduce a new cell-based points-to analysis which more precisely handles heap data structures and type-unsafe operations like pointer arithmetic and pointer casting. We give experimental results on benchmarks from the software verification competition using the program verification framework in Cascade. We show that a partitioned memory model using our cell-based points-to analysis outperforms models using other analyses.
Wei Wang, Clark Barrett, Thomas Wies


Weitere Informationen

Premium Partner