Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques

G Hagen; C Tinelli

doi:10.1109/FMCAD.2008.ECP.19

Back

Conference proceeding

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques

G Hagen and C Tinelli

2008 Formal Methods in Computer-Aided Design, pp.1-9

11/2008

DOI: 10.1109/FMCAD.2008.ECP.19

View Online

Abstract

We present a general approach for verifying safety properties of Lustre programs automatically. Key aspects of the approach are the choice of an expressive first-order logic in which Lustre's semantics is modeled very naturally, the tailoring to this logic of SAT-based k-induction and abstraction techniques, and the use of SMT solvers to reason efficiently in this logic. We discuss initial experimental results showing that our implementation of the approach is highly competitive with existing verification solutions for Lustre.

Arithmetic

Computer science

Embedded system

Formal verification

Logic

Manufacturing industries

Safety

Software tools

Specification languages

Surface-mount technology

Details

Title: Subtitle: Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques
Creators: G Hagen - University of Iowa
C Tinelli - University of Iowa
Resource Type: Conference proceeding
Publication Details: 2008 Formal Methods in Computer-Aided Design, pp.1-9
DOI: 10.1109/FMCAD.2008.ECP.19
Publisher: IEEE
Language: English
Date published: 11/2008
Academic Unit: Computer Science
Record Identifier: 9984259408802771

Metrics

13 Record Views