Automatic Symbolic Verification of Embedded Systems

R. Alur,T. Henzinger,Pei-Hsin Ho

Published 1996 in IEEE Trans. Software Eng.

ABSTRACT

No abstract is available for this paper.

PUBLICATION RECORD

Publication year
1996
Venue
IEEE Trans. Software Eng.
Publication date
1996-03-01
Fields of study
Computer Science, Engineering
Identifiers
DOI 10.1109/32.489079
External record
Open on Semantic Scholar
Source metadata
Semantic Scholar

CITATION MAP

EXTRACTION MAP

CLAIMS

No claims are published for this paper.

CONCEPTS

No concepts are published for this paper.

REFERENCES

Algorithmic Analysis of Nonlinear Hybrid Systems
1998cited by this paper
The Beneets of Relaxing Punctuality
1996cited by this paper
Automatic Analysis of Hybrid Systems
1996cited by this paper
Timing Analysis in COSPAN
1996cited by this paper
The symbolic model-checking for real-time systems
1996cited by this paper
Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems
1996cited by this paper
Compositional and symbolic model-checking of real-time systems
1995cited by this paper
A User Guide to HyTech
1995cited by this paper
HYTECH: the next generation
1995cited by this paper
What's decidable about hybrid automata?
1995cited by this paper
Hybrid Automata with Finite Bisimulatioins
1995cited by this paper
Two examples of verification of multirate timed automata with Kronos
1995cited by this paper
Symbolic approximations for verifying real-time systems
1995cited by this paper
The Algorithmic Analysis of Hybrid Systems
1995cited by this paper
Automated Analysis of an Audio Control Protocol
1995cited by this paper
Computing simulations on finite and infinite graphs
1995cited by this paper
Modeling and analysis of real-time Ada tasking programs
1994cited by this paper
A Note on Abstract Interpretation Strategies for Hybrid Automata
1994cited by this paper
A Theory of Timed Automata
1994cited by this paper
Verification of Linear Hybrid Systems by Means of Convex Approximations
1994cited by this paper
HYTECH: The Cornell HYbrid TECHnology Tool
1994cited by this paper
Symbolic Model Checking
1993cited by this paper
On model checking for real-time properties with durations
1993cited by this paper
Automatic Veriication of Nite-state Concurrent Systems Using Temporal-logic Speciications. Acm
1993cited by this paper
Parametric real-time reasoning
1993cited by this paper
Model-Checking in Dense Real-time
1993cited by this paper
Delay Analysis in Synchronous Programs
1993cited by this paper
An Approach to the Description and Analysis of Hybrid Systems
1992cited by this paper
Symbolic model checking for real-time systems
1992cited by this paper
Symbolic model checking
1992cited by this paper
Integration Graphs: A Class of Decidable Hybrid Systems
1992cited by this paper
Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems
1992cited by this paper
The benefits of relaxing punctuality
1991cited by this paper
From Timed to Hybrid Systems
1991cited by this paper
A Calculus of Durations
1991cited by this paper
A really temporal logic
1989cited by this paper
Timing Assumptions and Verification of Finite-State Concurrent Systems
1989cited by this paper
Mathematica--A System for Doing Mathematics by Computer.
1989cited by this paper
Mathematica - a system for doing mathematics by computer
1988cited by this paper
A fast mutual exclusion algorithm
1987cited by this paper
Automatic verification of finite-state concurrent systems using temporal logic specifications
1986cited by this paper
Checking that finite state concurrent programs satisfy their linear specification
1985cited by this paper
Specification and verification of concurrent systems in CESAR
1982cited by this paper
A Decision Procedure for the First Order Theory of Real Addition with Order
1975cited by this paper

CITED BY

Explaining Unsolvability of Planning Problems in Cyber-Physical Systems
2025cites this paper
Model Checking Linear Temporal Properties on Polyhedral Systems
2024cites this paper
A possible worlds semantics for trustworthy non-deterministic computations
2024cites this paper
On the Trade-off Between Efficiency and Precision of Neural Abstraction
2023cites this paper
Safety Verification of Decision-Tree Policies in Continuous Time
2023cites this paper
Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation
2022cites this paper
Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System
2022cites this paper
Foundational Response-Time Analysis as Explainable Evidence of Timeliness
2022cites this paper
Proof-checking Bias in Labeling Methods
2022cites this paper
CREST – a DSML for hybrid CPS modelling
2021cites this paper
Chapter 30: Verification of Hybrid Systems
2021cites this paper
Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study
2021cites this paper
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
2020cites this paper
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
2020cites this paper
Ecosystems of Software Engineering
2020cites this paper
Trustworthy AI
2020cites this paper
Safety Properties of Hybrid System Product Lines
2020cites this paper
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic
2020influential citation
Formal modeling and performance evaluation for hybrid systems: a probabilistic hybrid process algebra-based approach
2020cites this paper
Refinements of behavioural abstractions for the supervisory control of hybrid systems
2020cites this paper
Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings
2020cites this paper
On the decidability of linear bounded periodic cyber-physical systems
2019cites this paper
Automatically verifying temporal properties of heap programs with cyclic proof
2019cites this paper
Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical Systems
2019cites this paper
Network Model of It-Infrastructure Resource Management
2019cites this paper
Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL (Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL)
2019cites this paper
From Bounded Reachability Analysis of Linear Hybrid Automata to Verification of Industrial CPS and IoT
2019cites this paper
Parametric Systems: Verification and Synthesis
2019influential citation
Automatic time-unbounded reachability analysis of hybrid systems
2019cites this paper
Deterministic Finite-Automata Abstractions of Time-Variant Sequential Behaviours
2018cites this paper
Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process. (Vérification formelle des systèmes cyber-physiques dans le processus industriel de la conception basée sur modèle)
2018cites this paper
Verification of Hybrid Systems
2018cites this paper
Formal verification and quantitative metrics of MPSoC data dynamics
2018cites this paper
Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans
2018cites this paper
Probabilistic bounded reachability for stochastic hybrid systems
2018cites this paper
Verifiably Safe Autonomy for Cyber-Physical Systems
2018cites this paper
Control of Industrial Systems to Avoid Failures: Application to Electrical System
2018cites this paper
Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories: an approach to verify safety properties in embedded and hybrid system models
2017cites this paper
Formally Correct Monitors for Hybrid Automata
2017cites this paper
Theorem proving based Formal Verification of Distributed Dynamic Thermal Management schemes
2017cites this paper
Tracking smooth trajectories in linear hybrid systems
2017cites this paper
Radboud Repository of the Radboud University
2017cites this paper
Counterexample-Guided Refinement of Template Polyhedra
2017cites this paper
A Framework to Reason about the Knowledge of Agents in Continuous Dynamic Systems
2017cites this paper
A Comparative Assessment of Collaborative Business Process Verification Approaches
2017cites this paper
International Workshop on Applied Verification for Continuous and Hybrid Systems Large-Scale Linear Systems from Order-Reduction ( Benchmark Proposal )
2017cites this paper
Formal verification of ECML hybrid models with spaceex
2017cites this paper
Linearizing Discrete-Time Hybrid Systems
2017cites this paper
On Reachability in Priced Probabilistic Timed Automata∗
2017cites this paper
Automatic Synthesis of Switching Controllers for Linear Hybrid Systems
2017influential citation
Formal Feature Interpretation of Hybrid Systems
2017influential citation
Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
2016cites this paper
On Expressiveness of TCTLΔh for Model Checking Distributed Systems
2016cites this paper
An Algorithmic Method for the Implantation of Detection-Resistant Covert Hardware Trojans
2016cites this paper
Design and Realization of Embedded System in Dangerous Chemical Warehouse Monitoring System
2016cites this paper
Deadness and how to disprove liveness in hybrid dynamical systems
2016cites this paper
A framework for verification of transaction level models in systemc
2016cites this paper
Formal verification of switched capacitor DC to DC power converter using circuit simulation traces
2016cites this paper
Extending Taylor Approximation to Hybrid Systems with Integrals
2016cites this paper
Bifurcation Analysis of Cardiac Alternans Using δ-Decidability
2016cites this paper
Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability
2016cites this paper
Limit Cycle Analysis in a Class of Hybrid Systems
2016cites this paper
Safety verification of finite real-time nonlinear hybrid systems using enhanced group preserving scheme
2016influential citation
A polynomial algorithm for diagnosability of fair discrete event systems
2015cites this paper
From non-zenoness verification to termination
2015cites this paper
PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior
2015cites this paper
Formal verification of control software
2015cites this paper
Eliminating spurious transitions in reachability with support functions
2015cites this paper
Modeling of Adaptive Cyber Physical Systems using Aspect-oriented Approach
2015cites this paper
Efficient Geometric Operations on Convex Polyhedra, with an Application to Reachability Analysis of Hybrid Systems
2015cites this paper
Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
2015influential citation
An initial categorization of foundational research in complex technical systems
2015cites this paper
An ETRI CPS Modeling Language for Specifying Hybrid Systems
2015cites this paper
Interrupt Timed Automata with Auxiliary Clocks and Parameters
2014cites this paper
Probabilistic verification of partially observable dynamical systems
2014cites this paper
Detecting Industrial Control Malware Using Automated PLC Code Analytics
2014cites this paper
Towards a Unified Theory of Timed Automata
2014cites this paper
Computable Analysis , Hybrid Automata , and Decision Procedures ( Extended Thesis Abstract )
2014cites this paper
No . NJU-SEG-2014-IJ-001 From Offline towards Real-time : A Hybrid System model Checking and CPS Co-Design Approach for Medical Device Plug-and-Play Collaborations
2014influential citation
Formal verification and simulation for platform screen doors and collision avoidance in subway control systems
2014influential citation
Symbolic orthogonal projections: a new polyhedral representation for reachability analysis of hybrid systems
2014cites this paper
Powertrain control verification benchmark
2014cites this paper
Model checking memory-related properties of hardware/software codesigns (Modelchecking Speicher-bezogener Eigenschaften für Hardware/Software Codesigns)
2014cites this paper
Non-convex Invariants and Urgency Conditions on Linear Hybrid Automata
2014cites this paper
Modular, hierarchical models of control systems in SpaceEx
2013cites this paper
Tracking differentiable trajectories across polyhedra boundaries
2013cites this paper
Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems
2013cites this paper
Model Checking Memory-Related Properties of Hardware/Software Co-designs
2013cites this paper
Formal verification of service-oriented adaptive driver assistance systems
2013cites this paper
A survey on temporal logics for specifying and verifying real-time systems
2013cites this paper
Formal Modelling, Analysis and Verification of Hybrid Systems
2013cites this paper
Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS: A hybrid formal modeling approach
2013cites this paper
Methodological Guidelines for Modelling and Design of Embedded Systems
2013cites this paper
Models for Real-Time Embedded Systems
2013cites this paper
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
2013influential citation
Dynamic verification of hybrid systems
2013cites this paper
Apricot - An Object-Oriented Modeling Language for Hybrid Systems
2013cites this paper
Provable Run Time Safety Assurance for a Non-Linear System
2013cites this paper
Tools for the Analysis of Hybrid Models
2013cites this paper
Automatic synthesis of switching controllers for linear hybrid systems: Safety control
2013influential citation