Nothing Special   »   [go: up one dir, main page]

Ciancia et al., 2017 - Google Patents

Model checking spatial logics for closure spaces

Ciancia et al., 2017

View PDF
Document ID
9457518130110019038
Author
Ciancia V
Latella D
Loreti M
Massink M
Publication year
Publication venue
Logical Methods in Computer Science

External Links

Snippet

Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to …
Continue reading at lmcs.episciences.org (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
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5068—Physical circuit design, e.g. layout for integrated circuits or printed circuit boards
    • G06F17/5081—Layout analysis, e.g. layout verification, design rule check
    • 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
    • G06F17/30587—Details of specialised database models
    • 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
    • G06N5/025—Extracting rules from data
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/04—Inference methods or devices
    • 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
    • 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
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F19/00—Digital computing or data processing equipment or methods, specially adapted for specific applications
    • G06F19/30—Medical informatics, i.e. computer-based analysis or dissemination of patient or disease data
    • G06F19/34—Computer-assisted medical diagnosis or treatment, e.g. computerised prescription or delivery of medication or diets, computerised local control of medical devices, medical expert systems or telemedicine
    • G06F19/345—Medical expert systems, neural networks or other automated diagnosis
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F15/00—Digital computers in general; Data processing equipment in general
    • G06F15/18—Digital computers in general; Data processing equipment in general in which a programme is changed according to experience gained by the computer itself during a complete run; Learning machines
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N7/00—Computer systems based on specific mathematical models
    • G06N7/005—Probabilistic networks
    • 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
    • G06F8/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • 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
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • 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
Ciancia et al. Model checking spatial logics for closure spaces
Ciancia et al. Specifying and verifying properties of space
Bartocci et al. Monitoring mobile and spatially distributed cyber-physical systems
Borrmann et al. Topological analysis of 3D building models using a spatial query language
Nenzi et al. Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
Queralt et al. OCL-Lite: Finite reasoning on UML/OCL conceptual schemas
Dvořák et al. Augmenting tractable fragments of abstract argumentation
Krings et al. SMT Solvers for Validation of B and Event-B models
Bresolin et al. Horn fragments of the Halpern-Shoham interval temporal logic
Bezhanishvili et al. Geometric model checking of continuous space
Ciancia et al. Spatial logic and spatial model checking for closure spaces
Gore et al. Augmenting bottom-up metamodels with predicates
Diallo et al. Toward a formalism of modeling and simulation using model theory
Bloch et al. Graph-based learning for automated code checking–Exploring the application of graph neural networks for design review
Dechter Tractable structures for constraint satisfaction problems
Loreti et al. A spatial logic for simplicial models
Gupta et al. A survey on concept-based approaches for model improvement
Cristiá et al. A decision procedure for sets, binary relations and partial functions
Mastromichalakis et al. Rule-Based Explanations of Machine Learning Classifiers Using Knowledge Graphs
He et al. A joint community detection model: Integrating directed and undirected probabilistic graphical models via factor graph with attention mechanism
Haarslev et al. SBox: A qualitative spatial reasoner—progress report
Vakili et al. Finite model finding using the logic of equality with uninterpreted functions
Keinänen Techniques for solving Boolean equation systems
Ma et al. Inferring with inconsistent OWL DL ontology: A multi-valued logic approach
Du et al. Qualitative spatial logics for buffered geometries