Sökning: "Automatic verification"

Visar resultat 1 - 5 av 65 avhandlingar innehållade orden Automatic verification.

1. 1. Parameterized Systems : Generalizing and Simplifying Automatic Verification

   Författare :Ahmed Rezine; Parosh Aziz Abdulla; Kedar Namjoshi; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Parameterized systems; Automatic verification; Approximation; Regular model checking; Safety; Termination; Computer science; Datavetenskap; Datavetenskap; Computer Science;

   Sammanfattning : In this thesis we propose general and simple methods for automatic verification of parameterized systems. These are systems consisting of an arbitrary number of identical processes or components. The number of processes defines the size of the system. LÄS MER

3. 2. Automatic Extraction of Program Models for Formal Software Verification

   Författare :Pedro de Carvalho Gomes; Dilian Gurov; Einar Johnsen; KTH; []
   Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Software Verification; Static Analysis; Program Models; Petri Nets; Compositional Verification; Concurrency; Computer Science; Datalogi;

   Sammanfattning : In this thesis we present a study of the generation of abstract program models from programs in real-world programming languages that are employed in the formal verification of software. The thesis is divided into three parts, which cover distinct types of software systems, programming languages, verification scenarios, program models and properties. LÄS MER

4. 3. Verification of Software under Relaxed Memory

   Författare :Carl Leonardsson; Bengt Jonsson; Parosh Aziz Abdulla; Mohamed Faouzi Atig; Viktor Vafeiadis; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; verification; relaxed memory models; Datavetenskap; Computer Science;

   Sammanfattning : The work covered in this thesis concerns automatic analysis of correctness of parallel programs running under relaxed memory models.When a parallel program is compiled and executed on a modern architecture, various optimizations may cause it to behave in unexpected ways. LÄS MER

5. 4. Procedure-Modular Verification of Temporal Safety Properties

   Författare :Siavash Soleimanifard; Dilian Gurov; Gerardo Schneider; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Modular Verification; Compositional Verification; Maximal Models; Model Checking; Temporal Properties;

   Sammanfattning : This thesis presents a fully automated technique for procedure-modular verification of control flow temporal safety properties. Procedure-modular verification is a natural instantiation of modular verification where modularity is achieved at the level of procedures. LÄS MER

7. 5. Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving

   Författare :Hans Svensson; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; distributed algorithms; fault-tolerance; theorem proving; verification; distributed programming; Erlang; model checking; testing;

   Sammanfattning : Software infiltrates every aspect of modern society. Production, transportation, entertainment, and almost every other sphere that influences modern living are either directly or indirectly dependent on software systems. LÄS MER