VerifyThis 2019: a program verification competition

International Journal on Software Tools for Technology Transfer ◽

10.1007/s10009-021-00619-x ◽

2021 ◽

Author(s):

Claire Dross ◽

Carlo A Furia ◽

Marieke Huisman ◽

Rosemary Monahan ◽

Peter Müller

Keyword(s):

Program Verification ◽

Automatic Verification ◽

Fully Automatic ◽

Human Aspect ◽

8Th Edition

AbstractVerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

Download Full-text

Fully automatic verification and error detection for parameterized iterative sequential circuits

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/3-540-61042-1_49 ◽

1996 ◽

pp. 258-277 ◽

Cited By ~ 4

Author(s):

Tiziana Margaria

Keyword(s):

Error Detection ◽

Sequential Circuits ◽

Automatic Verification ◽

Fully Automatic

Download Full-text

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_8 ◽

2021 ◽

pp. 131-147

Author(s):

Alessandro Cimatti ◽

Alberto Griggio ◽

Gianluca Redondi

Keyword(s):

Communication Protocols ◽

Order Logic ◽

Automatic Verification ◽

First Order Logic ◽

Transition Systems ◽

Fully Automatic ◽

And Control ◽

Inductive Invariants ◽

Automatic Technique ◽

Parametric Systems

AbstractThe problem of invariant checking in parametric systems – which are required to operate correctly regardless of the number and connections of their components – is gaining increasing importance in various sectors, such as communication protocols and control software. Such systems are typically modeled using quantified formulae, describing the behaviour of an unbounded number of (identical) components, and their automatic verification often relies on the use of decidable fragments of first-order logic in order to effectively deal with the challenges of quantified reasoning.In this paper, we propose a fully automatic technique for invariant checking of parametric systems which does not rely on quantified reasoning. Parametric systems are modeled with array-based transition systems, and our method iteratively constructs a quantifier-free abstraction by analyzing, with SMT-based invariant checking algorithms for non-parametric systems, increasingly-larger finite instances of the parametric system. Depending on the verification result in the concrete instance, the abstraction is automatically refined by leveraging canditate lemmas from inductive invariants, or by discarding previously computed lemmas.We implemented the method using a quantifier-free SMT-based IC3 as underlying verification engine. Our experimental evaluation demonstrates that the approach is competitive with the state of the art, solving several benchmarks that are out of reach for other tools.

Download Full-text

TU-H-CAMPUS-JeP1-02: Fully Automatic Verification of Automatically Contoured Normal Tissues in the Head and Neck

Medical Physics ◽

10.1118/1.4957670 ◽

2016 ◽

Vol 43 (6Part37) ◽

pp. 3778-3778 ◽

Cited By ~ 2

Author(s):

R McCarroll ◽

B Beadle ◽

J Yang ◽

L Zhang ◽

M Mejia ◽

...

Keyword(s):

Head And Neck ◽

Automatic Verification ◽

Normal Tissues ◽

Fully Automatic

Download Full-text

A new method of complex structure analysis by electron microscopy

Proceedings, annual meeting, Electron Microscopy Society of America ◽

10.1017/s0424820100110283 ◽

1978 ◽

Vol 36 (1) ◽

pp. 628-629

Author(s):

V.V. Rybin ◽

E.V. Voronina

Keyword(s):

Complex Structure ◽

Reciprocal Lattice ◽

Stacking Faults ◽

Plastic Strains ◽

Base Position ◽

Structural Regularity ◽

Orientation Matrix ◽

Computerized Processing ◽

Fully Automatic ◽

Diffraction Patterns

Recently, it has become essential to develop a helpful method of the complete crystallographic identification of fine fragmented crystals. This was maainly due to the investigation into structural regularity of large plastic strains. The method should be practicable for determining crystallographic orientation (CO) of elastically stressed micro areas of the order of several micron fractions in size and filled with λ>1010 cm-2 density dislocations or stacking faults. The method must provide the misorientation vectors of the adjacent fragments when the angle ω changes from 0 to 180° with the accuracy of 0,3°. The problem is that the actual electron diffraction patterns obtained from fine fragmented crystals are the superpositions of reflections from various fragments, though more than one or two reflections from a fragment are hardly possible. Finally, the method should afford fully automatic computerized processing of the experimental results.The proposed method meets all the above requirements. It implies the construction for a certain base position of the crystal the orientation matrix (0M) A, which gives a single intercorrelation between the coordinates of the unity vector in the reference coordinate system (RCS) and those of the same vector in the crystal reciprocal lattice base : .

Download Full-text