Logic in Computer Science
From MaRDI portal
data structuremodel checkingmodal logicnatural deductiontextbookBoolean functionsmultiagent systemspredicate logicprogram verificationpropositional logicSAT solverbinary decision diagramslogic of knowledgeobject modelingcontract-programming paradigm
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)
Recommendations
Cited in
(81)- Reasoning about truth in first-order logic
- NOTIONAL LOGIC OF SYSTEMS
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- A framework for compositional nonblocking verification of extended finite-state machines
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- A process calculus for privacy-preserving protocols in location-based service systems
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- Abstraction and approximation in fuzzy temporal logics and models
- Verification of asynchronous systems with an unspecified component
- Machine learning for first-order theorem proving
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Formalizing a hierarchical file system
- Modal operators on pseudo-BE algebras
- Completeness for recursive procedures in separation logic
- A linear translation from CTL^* to the first-order modal -calculus
- Safe autonomy under perception uncertainty using chance-constrained temporal logic
- Characterizing and extending answer set semantics using possibility theory
- Merging Procedural and Declarative Proof
- Parallelizing SMT solving: lazy decomposition and conciliation
- Typed context awareness ambient calculus for pervasive applications
- Formalizing a hierarchical file system
- Kripke modelling and verification of temporal specifications of a multiple UAV system
- A Refined Resolution Calculus for CTL
- The Complexity of Linear-Time Temporal Logic Model Repair
- Formalized proof systems for propositional logic
- scientific article; zbMATH DE number 7447760 (Why is no real title available?)
- Modelling mutual exclusion in a process algebra with time-outs
- Temporal normal form for linear temporal logic formulae
- Indexed and fibered structures for partial and total correctness assertions
- A formalism to specify unambiguous instructions inspired by Mīmāṁsā in computational settings
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
- Describing the what and why of students' difficulties in Boolean logic
- An accessible verification environment for UML models of services
- Verifying the consistency of web-based technical documentations
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization
- Why there is no general solution to the problem of software verification
- A two-level approach based on model checking to support architecture conformance checking
- Synthesis of obfuscation policies to ensure privacy and utility
- scientific article; zbMATH DE number 7453963 (Why is no real title available?)
- Linear temporal logic symbolic model checking
- Representation theorems in computer science. A treatment in logic engineering
- Probabilistic (logic) programming concepts
- Performability assessment by model checking of Markov reward models
- On the benefits of knowledge compilation for feature-model analyses
- Tractable representations for Boolean functional synthesis
- Formalising the double-pushout approach to graph transformation
- Global view on reactivity: switch graphs and their logics
- Are bundles good deals for first-order modal logic?
- Knowledge and Games in Modal Semirings
- Model checking the observational determinism security property using PROMELA and SPIN
- A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes
- Specification and Verification of Multi-Agent Systems
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Fair multi-party contract signing using private contract signatures
- Comparative analysis of statistical model checking tools
- Complexity of finite-variable fragments of propositional temporal and modal logics of computation
- Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction
- Hoare logic-based genetic programming
- Diagnosability of delay-deadline failures in fair real time discrete event models
- Formal modeling and verification for MVB
- Computational logic: its origins and applications
- Quantified epistemic logics for reasoning about knowledge in multi-agent systems
- scientific article; zbMATH DE number 7809761 (Why is no real title available?)
- Keeping calm in the face of change. Towards optimisation of FRP by reasoning about change
- Generalized qualitative spatio-temporal reasoning: complexity and tableau method
- scientific article; zbMATH DE number 1446599 (Why is no real title available?)
- Yet another kind of rough sets induced by coverings
- Keeping logic in the trivium of computer science: a teaching perspective
- Thinking programs. Logical modeling and reasoning about languages, data, computations, and executions
- On the computation of counterexamples in compositional nonblocking verification
- Linear temporal logic vehicle routing with applications to multi-UAV mission planning
- A resolution calculus for the branching-time temporal logic CTL
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- An environment for specifying and model checking mobile ring robot algorithms
- Construction of parametric barrier functions for dynamical systems using interval analysis
- Practical verification of multi-agent systems against \textsc{Slk} specifications
- A Spatial Logic for Simplicial Models
- Model checking of robot gathering
This page was built for publication: Logic in Computer Science
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4830107)
