arXiv subjects

Cristina David

Publications and source records attributed to Cristina David.

26 records · Page 2Linked to original sources

arXiv2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature.

eess.SY↗

arXiv2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.

eess.SY↗

arXiv2015

Using Program Synthesis for Program Analysis

In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the {\it synthesis fragment}. Satisfiability of a formula in the synthesis fragment is decidable over finite domains; specifically the decision problem is NEXPTIME-complete. If a formula in this fragment is satisfiable, a solution consists of a satisfying assignment from the second order variables to \emph{functions over finite domains}. To concretely find these solutions, we synthesise \emph{programs} that compute the functions. Our program synthesis algorithm is complete for finite state programs, i.e. every \emph{function} over finite domains is computed by some \emph{program} that we can synthesise. We can therefore use our synthesiser as a decision procedure for the synthesis fragment of second-order logic, which in turn allows us to use it as a powerful backend for many program analysis tasks. To show the tractability of our approach, we evaluate the program synthesiser on several static analysis problems.

cs.LO↗

arXiv2015

Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)

Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities such as denial-of-service attacks. To make termination checks scale to large systems, interprocedural termination analysis seems essential, which is a largely unexplored area of research in termination analysis, where most effort has focussed on difficult single-procedure problems. We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show that our tool 2LS outperforms state-of-the-art alternatives, and demonstrate the clear advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.

cs.SE↗

arXiv2015

Danger Invariants

Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Fundamentally, such analysers summarise traces into sets of states, thus trading the ability to distinguish traces for computational tractability. Conversely, static bug finders (e.g. Bounded Model Checking) give evidence for the failure of an assertion in the form of a counterexample, which can be inspected by the user. However, static bug finders fail to scale when analysing programs with bugs that require many iterations of a loop as the computational effort grows exponentially with the depth of the bug. We propose a novel approach for finding bugs, which delivers the performance of abstract interpretation together with the concrete precision of BMC. To do this, we introduce the concept of danger invariants -- the dual to safety invariants. Danger invariants summarise sets of traces that are guaranteed to reach an error state. This summarisation allows us to find deep bugs without false alarms and without explicitly unwinding loops. We present a second-order formulation of danger invariants and use the Second-Order SAT solver described in previous work to compute danger invariants for intricate programs taken from the literature.

cs.PL↗

arXiv2015

Second-Order Propositional Satisfiability

Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentially, the heuristic reduces a second-order problem to a first-order/propositional one, while the validation is often just a call to a SAT/SMT solver. This results in a monolithic design of such analyses that conflates the formulation of the problem with the solving process. Consequently, any change to the latter causes changes to the whole analysis. This design is dictated by the state of the art in solver technology. While SAT/SMT solvers have experienced tremendous progress, there are barely any second-order solvers. This paper takes a step towards addressing this situation by proposing a decidable fragment of second-order logic that is still expressive enough to capture numerous program analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We refer to the satisfiability problem for this fragment as Second-Order SAT and show it is NEXPTIME-complete. Finally, we build a decision procedure for Second-Order SAT based on program synthesis and present experimental evidence that our approach is tractable for program analysis problems.

cs.LO↗

arXiv2014

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs

This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we propose the theory SLH of singly-linked lists with length, which is able to capture non-trivial interactions between shape and arithmetic. When using the theory of bit-vector arithmetic as a background, SLH is efficiently decidable via a reduction to SAT. We show the utility of SLH for software verification by using it to express safety invariants and termination arguments for programs manipulating potentially cyclic, singly-linked lists with unrestricted, unspecified sharing. We also provide an implementation of the decision procedure and use it to check safety and termination proofs for several heap-manipulating programs.

cs.LO↗

arXiv2014

Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs

Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking functions over mathematical integers. This class of functions is insufficient for proving termination of many terminating programs, and furthermore a termination argument for a program operating on mathematical integers does not always lead to a termination argument for the same program operating on fixed-width machine integers. We propose a termination analysis able to generate nonlinear, lexicographic ranking functions and nonlinear recurrence sets that are correct for fixed-width machine arithmetic and floating-point arithmetic Our technique is based on a reduction from program \emph{termination} to second-order \emph{satisfaction}. We provide formulations for termination and non-termination in a fragment of second-order logic with restricted quantification which is decidable over finite domains. The resulted technique is a sound and complete analysis for the termination of finite-state programs with fixed-width integers and IEEE floating-point arithmetic.

cs.LO↗