Catálogo de publicaciones - libros

In 1999 three formal-methods researchers, including the speaker, founded a company to commercialize formal modeling and verification technology for envisioned telecommunications customers. Eight years later, the company sells testing tools to embedded control software developers in the automotive, aerospace and related industries. This talk will describe the journey taken by the company during its evolution, why this journey was both less and more far than it seems, and how the speaker’s views on the practical utility of mathematically oriented software research changed along the way.

A program verification system for modern software uses a host of technologies, like programming language semantics, formalization of good programming idioms, inference techniques, verification-condition generation, and theorem proving. In this talk, I will survey these techniques from the perspective of the Spec# programming system, of which I will also give a demo. I will reflect on some lessons learned from building automatic program verifiers, as well as highlight a number of remaining challenges.

Programs commonly maintain multiple linked data structures. Correlations between multiple data structures may often be . In this paper, we show how this between different (singly-linked) data structures can be utilized to perform shape analysis and verification more efficiently. We present a new abstraction based on decomposing graphs into sets of subgraphs, and show that, in practice, this new abstraction leads to very little loss of precision, while yielding substantial improvements to efficiency.

Reasoning about heap-allocated data structures such as linked lists and arrays is challenging. The predicate has proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. Sound and precise analysis for such data structures becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software.

In this paper, we give a novel formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present preliminary experience with a prototype verifier on a set of illustrative C benchmarks.

Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. This paper presents Deryaft, a novel algorithm for generating likely of structurally complex data. Given a small set of concrete structures, Deryaft analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, Deryaft focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph.

Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application.

We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, , and given multiple linear-time (-regular or LTL) properties , and probabilities  ∈ [0,1],  = 1,...,, we ask whether there exists a strategy for the controller such that, for all , the probability that a trajectory of controlled by satisfies is at least . We provide an algorithm that decides whether there exists such a strategy and if so produces it, and which runs in time polynomial in the size of the MDP. Such a strategy may require the use of both randomization and memory. We also consider more general multi-objective -regular queries, which we motivate with an application to assume-guarantee compositional reasoning for probabilistic systems.

Note that there can be trade-offs between different properties: satisfying property with high probability may necessitate satisfying with low probability. Viewing this as a multi-objective optimization problem, we want information about the “trade-off curve” or for maximizing the probabilities of different properties. We show that one can compute an approximate Pareto curve with respect to a set of -regular properties in time polynomial in the size of the MDP.

Our quantitative upper bounds use LP methods. We also study qualitative multi-objective model checking problems, and we show that these can be analysed by purely graph-theoretic methods, even though the strategies may still require both randomization and memory.

This paper describes PReMo, a tool for analyzing Recursive Markov Chains, and their controlled/game extensions: (1-exit) Recursive Markov Decision Processes and Recursive Simple Stochastic Games.

This paper considers algorithms for counterexample generation for (bounded) probabilistic reachability properties in fully probabilistic systems. Finding the strongest evidence (i.e, the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that are mostly deviating from the required probability bound can be computed by adopting (partially new hop-constrained) shortest paths algorithms that dynamically determine .

This paper studies the effect of bisimulation minimisation in model checking of monolithic discrete-time and continuous-time Markov chains as well as variants thereof with rewards. Our results show that—as for traditional model checking—enormous state space reductions (up to logarithmic savings) may be obtained. In contrast to traditional model checking, in many cases, the verification time of the original Markov chain exceeds the quotienting time plus the verification time of the quotient. We consider probabilistic bisimulation as well as versions thereof that are tailored to the property to be checked.

We define a novel formulation of dataflow analysis for concurrent programs, where the flow of facts is along the dependencies of events. We capture the control flow of concurrent programs using a Petri net (called the ), develop algorithms based on partially-ordered unfoldings, and report experimental results for solving causal dataflow analysis problems. For the subclass of distributive problems, we prove that complexity of checking data flow is linear in the number of facts and in the of the control net.