[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Křena et al., 2013 - Google Patents

Automated formal analysis and verification: an overview

Křena et al., 2013

View PDF
Document ID
13082519740066573333
Author
Křena B
Vojnar T
Publication year
Publication venue
International Journal of General Systems

External Links

Snippet

This paper provides an overview of various existing approaches to automated formal analysis and verification. The most space is devoted to the approach of model checking, including its basic principles as well as the different techniques that have been proposed for …
Continue reading at www.fit.vutbr.cz (PDF) (other versions)

Classifications

    • 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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • 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/3612—Software analysis for verifying properties of programs by runtime analysis
    • 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
    • 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
    • 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
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • 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
    • 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/20—Handling natural language data
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/07—Error detection; Error correction; Monitoring responding to the occurence of a fault, e.g. fault tolerance
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/70—Software maintenance or management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • 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
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management

Similar Documents

Publication Publication Date Title
Kanewala et al. Predicting metamorphic relations for testing scientific software: a machine learning approach using graph kernels
EP3458953B1 (en) Systems and methods for model-based analysis of software
Li et al. Two decades of Web application testing—A survey of recent advances
Aronis et al. Optimal dynamic partial order reduction with observers
US20130339930A1 (en) Model-based test code generation for software testing
Farzan et al. Automated hypersafety verification
US20200210158A1 (en) Automated or machine-enhanced source code debugging
Sinha et al. Staged concurrent program analysis
Morse et al. Model checking LTL properties over ANSI-C programs with bounded traces
KP et al. Finite‐state model extraction and visualization from Java program execution
Havelund et al. Runtime verification logics a language design perspective
Chamillard An empirical comparison of static concurrency analysis techniques
Inverso et al. Bounded verification of multi-threaded programs via lazy sequentialization
Sherman et al. Structurally defined conditional data-flow static analysis
Donaldson et al. Automatic analysis of scratch-pad memory code for heterogeneous multicore processors
Křena et al. Automated formal analysis and verification: an overview
Allamigeon Static analysis of memory manipulations by abstract interpretation--Algorithmics of tropical polyhedra, and application to abstract interpretation
Simons et al. A verified and optimized Stream X‐Machine testing method, with application to cloud service certification
Beebe A complete bibliography of publications in science of computer programming
Milewicz et al. Refinement of structural heuristics for model checking of concurrent programs through data mining
Bakhirkin et al. A forward analysis for recurrent sets
Ingves Vägar mot ett svenskt ordförråd: Nyanlända ungdomars ordförrådsutveckling på språkintroduktionsprogrammet
Afanador A Benchmark Framework and Support for At-scale Binary Vulnerability Analysis
Even-Mendoza et al. Lattice-based refinement in bounded model checking
Duan et al. Verifying temporal properties of c programs via lazy abstraction