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
Nenzi et al. Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
Dvořák et al. Augmenting tractable fragments of abstract argumentation
Scheider et al. Ontology of core concept data types for answering geo-analytical questions
Krings et al. SMT Solvers for Validation of B and Event-B models
Diallo et al. Toward a formalism of modeling and simulation using model theory
Dechter Tractable structures for constraint satisfaction problems
Bloch et al. Graph-based learning for automated code checking–Exploring the application of graph neural networks for design review
Cristiá et al. A decision procedure for sets, binary relations and partial functions
Loreti et al. A spatial logic for simplicial models
Hekmatnejad et al. Formalizing and evaluating requirements of perception systems for automated vehicles using spatio-temporal perception logic
Vörös et al. Industrial applications of the PetriDotNet modelling and analysis tool
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
Le et al. A certified decision procedure for tree shares
Du et al. Qualitative spatial logics for buffered geometries
Keinänen Techniques for solving Boolean equation systems
Hummel Description logic for scene understanding at the example of urban road intersections
IMT Model Checking Spatial Logics for Closure Spaces-Extended Version
Ma et al. Inferring with inconsistent OWL DL ontology: A multi-valued logic approach
Toman et al. Applications and extensions of PTIME description logics with functional constraints
Dimovski et al. Family-based model checking of fMultiLTL properties
Mastromichalakis et al. Rule-Based Explanations of Machine Learning Classifiers Using Knowledge Graphs