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

Finkel et al., 2020 - Google Patents

Verification of flat FIFO systems

Finkel et al., 2020

View PDF
Document ID
16448796344760869303
Author
Finkel A
Praveen M
Publication year
Publication venue
Logical Methods in Computer Science

External Links

Snippet

The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded …
Continue reading at lmcs.episciences.org (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/3668—Software testing
    • 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/30943—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type
    • G06F17/30946—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type indexing structures
    • 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
    • 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
    • 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/46—Multiprogramming arrangements
    • 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
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • 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
    • 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

Similar Documents

Publication Publication Date Title
Basin et al. CryptHOL: Game-based proofs in higher-order logic
Bryant Binary decision diagrams
Cook The P versus NP problem
Finkel et al. Verification of flat FIFO systems
Blumensath et al. Finite presentations of infinite structures: Automata and interpretations
Barrett et al. A Generalization of Shostak# x2019; s Method for Combining Decision Procedures
Walukiewicz A landscape with games in the background
Kuske et al. Communicating automata.
Kiefer et al. Language equivalence for probabilistic automata
Finkbeiner et al. Collecting statistics over runtime executions
Bozga et al. Flat parametric counter automata
Mousavi et al. On the complexity of zero gap MIP
Canetti et al. Analyzing security protocols using time-bounded task-PIOAs
Lipton et al. Amplifying circuit lower bounds against polynomial time, with applications
Demri Linear-time temporal logics with Presburger constraints: an overview★
FINKEL et al. VERIFICATION OF FLAT FIFO MACHIN.
Bozga et al. On decidability within the arithmetic of addition and divisibility
Dang et al. Composability of infinite-state activity automata
Abdulla et al. R-automata
Ibarra et al. Reachability analysis for some models of infinite-state transition systems
Exibard et al. Computability of Data-Word Transductions over Different Data Domains
To Model checking FO (R) over one-counter processes and beyond
Bergstra et al. Network algebra for asynchronous dataflow
Bollig et al. Branch-Well-Structured Transition Systems and Extensions
Nowak et al. Formal security proofs with minimal fuss: Implicit computational complexity at work