[go: up one dir, main page]

Bendík et al., 2018 - Google Patents

Online enumeration of all minimal inductive validity cores

Bendík et al., 2018

View PDF
Document ID
7473810819466518741
Author
Bendík J
Ghassabani E
Whalen M
Černá I
Publication year
Publication venue
International Conference on Software Engineering and Formal Methods

External Links

Snippet

Symbolic model checkers can construct proofs of safety properties over complex models, but when a proof succeeds, the results do not generally provide much insight to the user. Minimal Inductive Validity Cores (MIVCs) trace a property to a minimal set of model elements …
Continue reading at jar-ben.github.io (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • G06F9/50—Allocation of resources, e.g. of the central processing unit [CPU]
    • G06F9/5061—Partitioning or combining of resources
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/445—Programme loading or initiating
    • G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F15/00—Digital computers in general; Data processing equipment in general
    • G06F15/16—Combinations of two or more digital computers each having at least an arithmetic unit, a programme unit and a register, e.g. for a simultaneous processing of several programmes
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F7/00—Methods or arrangements for processing data by operating upon the order or content of the data handled
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N99/00—Subject matter not provided for in other groups of this subclass
    • G06N99/005—Learning machines, i.e. computer in which a programme is changed according to experience gained by the machine itself during a complete run

Similar Documents

Publication Publication Date Title
Komuravelli et al. SMT-based model checking for recursive programs
Alur et al. Predicate abstraction for reachability analysis of hybrid systems
Lahiri et al. Constructing quantified invariants via predicate abstraction
Bouajjani et al. Bounded phase analysis of message-passing programs
Bendík et al. Online enumeration of all minimal inductive validity cores
Morse et al. Model checking LTL properties over ANSI-C programs with bounded traces
Skeirik et al. A constructor-based reachability logic for rewrite theories
Bak et al. Rigorous simulation-based analysis of linear hybrid systems
Macedo et al. Pardinus: A temporal relational model finder
Neele et al. Solving parameterised boolean equation systems with infinite data through quotienting
Winkler et al. Runtime complexity analysis of logically constrained rewriting
Bacci et al. Converging from branching to linear metrics on Markov chains
Xie et al. SAT–LP–IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
Badban et al. Test automation for hybrid systems
Bae et al. Guarded terms for rewriting modulo SMT
Chatterjee et al. Distributed bounded model checking
Bueno et al. euforia: Complete software model checking with uninterpreted functions
Cabodi et al. To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking
Sharma et al. A new abstraction framework for affine transformers
Leucker et al. A new refinement strategy for CEGAR-based industrial model checking
Havlena et al. Complementation of Emerson-Lei Automata
Abdulla Regular model checking: Evolution and perspectives
Schordan et al. Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges
Cimatti et al. Infinite-state liveness checking with rlive
Burch et al. Symbolic model checking for sequential circuit verification