Titlebook: Hardware and Software: Verification and Testing; 13th International H Ofer Strichman,Rachel Tzoref-Brill Conference proceedings 2017 Spring

混杂人

Substance-Abuse

智力高

Trace-Based Run-Time Analysis of Message-Passing Go Programsethod to trace communication events during execution. A model of the dependencies among events can be constructed to identify potential bugs. Compared to the vector clock method, our approach is much simpler and has in general a significant lower run-time overhead. A further advantage is that we als

旧石器时代

尽责

圣人

SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systemss. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dyna

MINT

A Symbolic Approach to Safety , Synthesisr. A popular language for providing such a specification is Linear Temporal Logic, or .. . synthesis in the general case has remained, however, a hard problem to solve in practice. Because of this, many works have focused on developing synthesis procedures for specific fragments of ., with an easier

GIBE

An Interaction Concept for Program Verification Systems with Explicit Proof Objectright guiding information is challenging for users and usually requires several reiterations. Supporting the user in this process can considerably reduce the effort of program verification..In this paper, we present an interaction concept for deductive program verification systems that combines poin

打火石

PRuning Through Satisfaction agressively by also removing certain branches for which there exist other branches that are more satisfiable. This is achieved by extending the popular conflict-driven clause learning (CDCL) paradigm with so-called ... We implemented our new paradigm, named . (SDCL), in the SAT solver .. Experiment

亚麻制品

LRA Interpolants from No Man’s Land). In particular when modelling programs with linear arithmetics, the standard state-of-the-art technique might provide either interpolants that are too specific or too generic to be useful for a given application. In this work we introduce the SI-LRA interpolation system for linear real arithmetics