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.
D-Finder tool implements a compositional method for the verification of component-based systems described in BIP language encompassing multi-party interaction. For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants.
A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are...
Static analysis by abstract interpretation [1] aims at automatically inferring properties on the behaviour of programs. We focus here on a specific kind of numerical invariants: the set of values taken by numerical variables, with a real numbers semantics, at each control point of a program.
In this paper we present InvGen, an automatic linear arithmetic invariant generator for imperative programs. InvGen’s unique feature is in its use of dynamic analysis to make invariant generation order of magnitude more efficient.
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties expressible...
BeepBeep is a lightweight runtime monitor for Ajax web applications. Interface specifications are expressed internally in an extension of LTL with first-order quantification; they can be transparently enforced on the client side using a small and invisible Java applet. Violations of the specification are reported on-the-fly and prevent erroneous or out-of-sequence XML messages from reaching the server.
We present Homer, an observational-equivalence model checker for the 3rd-order fragment of Idealized Algol (IA) augmented with iteration. It works by first translating terms of the fragment into a precise representation of their game semantics as visibly pushdown automata (VPA). The VPA-translates are then passed to a VPA toolkit (which we have implemented) to test for equivalence. Thanks to the fully...
This article describes Apron, a freely available library dedicated to the static analysis of the numerical variables of programs by abstract interpretation. Its goal is threefold: provide analysis implementers with ready-to-use numerical abstractions under a unified API, encourage the research in numerical abstract domains by providing a platform for integration and comparison, and provide teaching...
We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifier-free finite-precision bit-vector logic (QF_BV). Beaver uses an eager approach, encoding the original SMT problem into a Boolean satisfiability (SAT) problem using a series of word-level and bit-level transformations. In this paper, we describe the most effective transformations, such as propagating constants...
Active testing has recently been introduced to effectively test concurrent programs. Active testing works in two phases. It first uses predictive off-the-shelf static or dynamic program analyses to identify potential concurrency bugs, such as data races, deadlocks, and atomicity violations. In the second phase, active testing uses the reports from these predictive analyses to explicitly control the...
While temporal logic in its various forms has proven essential to reason about reactive systems, agent-based scenarios are typically specified by considering high-level agents attitudes. In particular, specification languages based on epistemic logic [7], or logics for knowledge, have proven useful in a variety of areas including robotics, security protocols, web-services, etc. For example, security...
In this paper, we present TASS which is a timing analyzer of scenario-based specifications. TASS accepts UML2.0 interaction models with general and expressive timing constraints and can be used for three kinds of timing analysis problems: the reachability analysis, the constraint conformance analysis, and the bounded delay analysis. The underlying technique of TASS is to reduce the timing analysis...
Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and generates optimized C code.
We present VS3, a tool that automatically verifies complex properties of programs and infers maximally weak preconditions and maximally strong postconditions by leveraging the power of SMT solvers. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS3 with a set of predicates and invariant templates. VS3 automatically finds instantiations...
Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed...
With the availability of multi-core processors and large-scale computing clusters, the study of parallel algorithms has been revived throughout the industry. We present a portfolio approach to deciding the satisfiability of SMT formulas, based on the recent success of related algorithms for the SAT problem. Our parallel version of Z3 outperforms the sequential solver, with speedups of well over an...
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.