The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another...
Abductive inference is a form of backwards logical reasoning that infers likely hypotheses from a given conclusion. In other words, given an invalid implication of the form A => B, abduction asks the question "What formula C do we need to conjoin with the antecedent A so that (i) A & C => B is logically valid and (ii) C is consistent with A?" Abductive reasoning has found many...
Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.
Synthesis is the question of how to construct a correct system from a specification. In recent years, synthesis has made major steps from a theoretists dream towards a practical design tool. While synthesis from a language like LTL has very high complexity, synthesis can be quite practical when we are willing to compromise on the specification formalism. Similarly, we can take a pragmatic approach...
The lack of appropriate models is often the biggest hurdle in applying formal methods in the industry. Creating executable models of industrial designs is a challenging task, one that we believe has not been sufficiently addressed by existing research. We address this problem for distributed message passing protocols by showing how to synthesize executable models of such protocols from transaction...
We present a new CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas, which we call the clausal abstraction. Each of the propositional formulas contains the variables of just one quantifier level and additional variables describing the interaction with adjacent quantifier levels. This decomposition leads to a simpler notion of refinement...
Acceleration is a technique for summarising loops by computing a closed-form representation of the loop behaviour. The closed form can be turned into an accelerator, which is a code snippet that skips over intermediate states of the loop to the end of the loop in a single step. Program analysers rely on invariant generation techniques to reason about loops. The state-of-the-art invariant generation...
Algebraic geometry is the study of the geometry of solutions to a system of multivariate polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the presence, absence, dimensions or intersection properties of the solution-sets, etc. Abstract and computational algebra is often used for this purpose - particularly...
In the early phases of the design of safety-critical systems, we need the ability to analyze the safety of different design solutions, comparing how different functional allocations impact the overall reliability of the system. To achieve this goal, we can apply formal techniques ranging from model checking to model-based fault-tree analysis. Using the results of the verification and safety analysis,...
In recent years, the inductive, incremental verification algorithm IC3 had a major impact on hardware model checking. Also with respect to software model checking, a number of adaptations of Boolean IC3 and combinations with CEGAR and ART-based techniques have been developed. However, most of them exploit the peculiarities of software programs, such as the explicit representation of control flow,...
Given a propositional formula F(x, y), a Skolem function for x is a function ψ (y), such that substituting ψ (y) for x in F gives a formula semantically equivalent to ∃x F. Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising circuits and bitvector programs from specifications,...
We address the problem of synthesizing efficient and correct synchronization for programs running under the C++ relaxed memory model. Given a finite-state program P and a safety property S such that P satisfies S under a sequentially consistent (SC) memory model, our approach automatically eliminates concurrency errors in P due to the relaxed memory model, by creating a new program P with additional...
IC3 is undoubtedly one of the most successful and important recent techniques for unbounded model checking. Understanding and improving IC3 has been a subject of a lot of recent research. In this regard, the most fundamental questions are how to choose Counterexamples to Induction (CTIs) and how to generalize them into (blocking) lemmas. Answers to both questions influence performance of the algorithm...
This paper presents a new method for automatically generating numerical invariants for imperative programs. The procedure computes a transition formula which overapproximates the behaviour of a given input program. It is compositional in the sense that it operates by decomposing the program into parts, computing a transition formula for each part, and then composing them. Transition formulas for loops...
In Satisfiability Modulo Theories (SMT), the theory of arrays provides operations to access and modify an array at a given index, e.g., read and write. However, common operations to modify multiple indices at once, e.g., memset or memcpy of the standard C library, are not supported. We describe algorithms to identify and extract array patterns representing such operations, including memset and memcpy...
Contemporary integrated circuits are complex system-on-chip (SoC) designs consisting of programmable cores along with accelerators and peripherals controlled by firmware running on the cores. The functionality of the SoC is implemented by a combination of firmware and hardware components. As a result, verifying these two components separately can miss bugs while attempting to formally verify the full...
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x1 ⩽ y + c, and describe that the value of x in the current state is at most the value of y in the previous state plus some constant c ϵ Z. In this paper, we argue that the complexity of imperative programs typically arises from counter increments and resets, which...
Reverse engineering is the extraction of word level information from a gate-level netlist. It has applications in formal verification, hardware trust, information recovery, and general technology mapping. A preprocessing step finds blocks in a circuit in which word level components are expected. A second step searches for word level components in these blocks. For this second step, we propose two...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.