How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Guillaume Petiot; Nikolaï Kosmatov; Alain Giorgetti; Jacques Julliand

doi:10.1007/978-3-319-09099-3_16

ScienceGate Book Chapters

BOOK-CHAPTER

How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Guillaume Petiot Nikolaï Kosmatov Alain Giorgetti Jacques Julliand

Year: 2014 Lecture notes in computer science Pages: 204-211 Publisher: Springer Science+Business Media

DOI: 10.1007/978-3-319-09099-3_16

Get Full-Text PDF Get Analytical Report

Keywords:

Computer science Concolic testing Software verification Programming language Plug-in Intelligent verification Set (abstract data type) Generator (circuit theory) Software engineering Verification Test (biology) Functional verification Software Formal verification Symbolic execution Software development Software construction

Metrics

Cited By

2.23

FWCI (Field Weighted Citation Impact)

Refs

0.85

Citation Normalized Percentile

Is in top 1%

Is in top 10%

Citation History

Topics

Software Testing and Debugging Techniques

Physical Sciences → Computer Science → Software

Formal Methods in Verification

Physical Sciences → Computer Science → Computational Theory and Mathematics

Security and Verification in Computing

Physical Sciences → Computer Science → Artificial Intelligence

How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Metrics

Citation History

Topics

Related Documents

Formal specification and automated verification of railway software with Frama-C

Typestates Specification and Verification in Frama-C

Guide to Software Verification with Frama-C

Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists

Specification and verification of simple logic control programs using Frama C