Sökning: "symbolic model checking"

Visar resultat 1 - 5 av 21 avhandlingar innehållade orden symbolic model checking.

  1. 1. Regular Model Checking

    Författare :Marcus Nilsson; Bengt Jonsson; Parosh Aziz Abdulla; Kim Larsen; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; formal methods; model checking; verification; regular sets; Computer science; Datavetenskap;

    Sammanfattning : A major current challenge in the area of program verification is to extend its applicability to infinite-state systems. A system can be infinite-state because it operates on unbounded data structures, such as queues, stacks, integers, etc., or because its description is parameterized by the number of components inside the system. LÄS MER

  3. 2. New Directions in Symbolic Model Checking

    Författare :Julien d'Orso; Parosh Abulla; Yassine Lakhnech; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Informatics; computer and systems science; Informatik; data- och systemvetenskap; Informatics; computer and systems science; Informatik; data- och systemvetenskap;

    Sammanfattning : In today's computer engineering, requirements for generally high reliability have pushed the notion of testing to its limits. Many disciplines are moving, or have already moved, to more formal methods to ensure correctness. This is done by comparing the behavior of the system as it is implemented against a set of requirements. LÄS MER

  4. 3. SAT Based Model Checking

    Författare :Niklas Een; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : This Thesis is a study of automatic reasoning about finite state machines (FSMs). Two techniques used in hardware verification are presented. In both, the verification is carried out by a translation of the problem into propositional logic. Satisfiability and validity of propositional formulas are decided by the use of a SAT solver. LÄS MER

  5. 4. Learning-based Software Testing using Symbolic Constraint Solving Methods

    Författare :Fei Niu; Karl Meinke; Reiner Hähnle; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Testing; Machine learning; Symbolic constraint solving; Model checking;

    Sammanfattning : Software testing remains one of the most important but expensive approaches to ensure high-quality software today. In order to reduce the cost of testing, over the last several decades, various techniques such as formal verification and inductive learning have been used for test automation in previous research. LÄS MER

  7. 5. Semantics, Decision Procedures, and Abstraction Refinement for Symbolic Trajectory Evaluation

    Författare :Jan-Willem Roorda; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Semantics; Abstraction; Satisfiability Solver; Symbolic Trajectory Evaluation; Formal Verification.; Model Checking;

    Sammanfattning : The rapid growth in hardware complexity has led to a need for formal verification of hardware designs to prevent bugs from entering the final silicon. Model-checking is a verification method in which a model of a system is checked against a property, describing the desired behaviour of the system over time. LÄS MER