VIS: A System for Verification and Synthesis

No abstract is available for this paper.

• Publication year

  1996

• Venue

  International Conference on Computer Aided Verification

• Publication date

  1996-08-03

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-61474-5_95
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking

  1995cited by this paper
• BDD Variable Ordering for Interacting Finite State Machines

  1994cited by this paper
• Efficient Formal Design Verification : Data Structure + Algorithms

  1994cited by this paper
• Compiling Verilog into Automata

  1994cited by this paper
• Interleaving based variable ordering methods for ordered binary decision diagrams

  1993cited by this paper
• SIS : A System for Sequential Circuit Synthesis

  1992influential reference
• The Verilog® Hardware Description Language

  1990cited by this paper
• Introduction to VLSI systems

  1978influential reference

• Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation And Its Linkage With Concrete Hardware Verification At Netlist Level

  2025cites this paper
• Image Computation for Quantum Transition Systems

  2025cites this paper
• Qsyn: A Developer-Friendly Quantum Circuit Synthesis Framework for NISQ Era and Beyond

  2024cites this paper
• Learning from Failures: Translation of Natural Language Requirements into Linear Temporal Logic with Large Language Models

  2024cites this paper
• Equivalence Checking for Flow-Based Computing

  2022cites this paper
• A systematic literature review on counterexample explanation

  2021influential citation
• A Mathematical Framework for Exploring Protein Folding Dynamics using Probabilistic Model Checking

  2020cites this paper
• Formally verified software countermeasures for control-flow integrity of smart card C code

  2019cites this paper
• Learning-based Testing for Automotive Embedded Systems

  2019cites this paper
• Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation

  2019cites this paper
• Improving Digital Circuit Simulation with Batch-Parallel Logic Evaluation

  2019influential citation
• Syntax-Guided Enumeration of Temporal Properties

  2019cites this paper
• Programming Is Modeling

  2018cites this paper
• MVL-MIN: A New Heuristic Minimization Tool For Multiple-valued Logic Functions

  2018cites this paper
• Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive Domain

  2018cites this paper
• Automatic Formal Verification of Digital Components of IoTs Using CBMC

  2018cites this paper
• Temporal Coverage Analysis for Dynamic Verification

  2018cites this paper
• Data layout oriented compilation techniques in vectorization for multi-/many-cores

  2017cites this paper
• INVITED: Safety guard: Runtime enforcement for safety-critical cyber-physical systems

  2017cites this paper
• Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement

  2017cites this paper
• NuDE 2.0: A Formal Method-based Software Development, Verification and Safety Analysis Environment for Digital I&Cs in NPPs

  2017influential citation
• INVITED: Safety Guards: Runtime Enforcement for Safety-Critical Cyber-Physical Systems

  2017cites this paper
• Multi-Valued Network Compaction using Redundancy Removal

  2017cites this paper
• A Case Study in Safety, Security, and Availability of Wireless-Enabled Aircraft Communication Networks

  2017cites this paper
• Word-level traversal of finite state machines using algebraic geometry

  2016cites this paper
• FBDtoVHDL: An Automatic Translation from FBD into VHDL for FPGA Development

  2016cites this paper
• GeNeDA: An Open-Source Workflow for Design Automation of Gene Regulatory Networks Inspired from Microelectronics

  2016cites this paper
• The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results

  2016cites this paper
• LTL Motion Planning with Collision Avoidance for A Team of Quadrotors

  2016cites this paper
• Unbounded safety verification for hardware using software analyzers

  2016cites this paper
• Formal Methods for Biological Systems: Languages, Algorithms, and Applications

  2016cites this paper
• Synthesizing Runtime Enforcer of Safety Properties Under Burst Error

  2016cites this paper
• Specification Format for Reactive Synthesis Problems

  2016cites this paper
• The Second Reactive Synthesis Competition (SYNTCOMP 2015)

  2016cites this paper
• A New Equivalence Checker for Demonstrating Correctness of Synthesis and Generation of Safety-Critical Software

  2016cites this paper
• Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization

  2016cites this paper
• Property Coverage Analysis Based Trustworthiness Verification for Potential Threats from EDA Tools

  2016cites this paper
• Automating Trace Buffer Post-Silicon Debug

  2016cites this paper
• Generating formal hardware verification properties from Natural Language documentation

  2015cites this paper
• The first reactive synthesis competition (SYNTCOMP 2014)

  2015cites this paper
• Combining Induction, Deduction, and Structure for Verification and Synthesis

  2015cites this paper
• Shield Synthesis: Runtime Enforcement for Reactive Systems

  2015influential citation
• UC Irvine UC Irvine Electronic Theses and Dissertations Title Generating Formal Verification Properties from Natural Language Hardware Specifications

  2015cites this paper
• Symbolic Model-Checking Using ITS-Tools

  2015cites this paper
• Toward Unification of Synthesis and Verification in Topologically Constrained Logic Design

  2015cites this paper
• A Verification Method for Single-Flux-Quantum Circuits Using Delay-Based Time Frame Model

  2015cites this paper
• HRELTL: A temporal logic for hybrid systems

  2015cites this paper
• Toward Unification of Synthesis andVerificationinTopologically Constrained Logic Design In this paper, the author presents a method by which logic synthesis and formal verification can be achieved with a small number of input patterns, if all possible circuit transformations are predetermined.

  2015cites this paper
• Formal verification of sequential Galois field arithmetic circuits using algebraic geometry

  2015cites this paper
• FSM-based properties and abstraction of components

  2014influential citation
• A Correctness Verification Technique for Commercial FPGA Synthesis Tools

  2014cites this paper
• Combining Symmetry Reduction with Generalized Symbolic Trajectory Evaluation

  2014cites this paper
• Improving the Efficiency and Quality of Omega-Regular Synthesis

  2014cites this paper
• Reasoning with Temporal Properties over Axioms of DL-Lite

  2014cites this paper
• Assistance au raffinement dans la conception des systèmes embarqués. (Assisting formal refinement and verification in embedded system design)

  2014cites this paper
• Preprint from Proceedings of IWLS 2004 , Temecula , USA , June 2004 Approximate Symbolic Model Checking for Incomplete Designs

  2014cites this paper
• 25 Years of Model Checking

  2014cites this paper
• An overview of model checking practices on verification of PLC software

  2014cites this paper
• From Löwenheim to PSL and SVA

  2014cites this paper
• Bounded model checking for asynchronous concurrent systems

  2014cites this paper
• Software Countermeasures for Control Flow Integrity of Smart Card C Codes

  2014cites this paper
• Experiments using XTA and ITS-tools

  2014cites this paper
• FSM-based properties and abstraction of components

  2014cites this paper
• NuDE 2.0: A model-based software development environment for the PLC & FPGA based digital systems in nuclear power plants

  2014cites this paper
• High-Level Simulation for Multiple Fault Injection Evaluation

  2014cites this paper
• An Integrated Software Development Framework for PLC & FPGA based Digital I&Cs

  2014cites this paper
• Using Natural Language Documentation in the Formal Verification of Hardware Designs

  2014cites this paper
• Verification of Generic Ubiquitous Middleware for Smart Home Using Coloured Petri Nets

  2014cites this paper
• Scalable Signal Selection for Post-Silicon Debug

  2013cites this paper
• Synthesis of Hierarchical Systems(Revised)

  2013cites this paper
• Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking

  2013cites this paper
• Using Abstraction to Guide the Search for Long Error Traces

  2013cites this paper
• Harnessing FPGA technology for rapid circuit debug

  2013cites this paper
• Combinational Logic Design Using Six-Terminal NEM Relays

  2013cites this paper
• Equivalence Checking between Pre-synthesis and Post-synthesis Programs by Using VIS

  2013cites this paper
• Correct low power design transformations for hardware systems

  2013cites this paper
• Multi-State Memory and Logic Designs Using Multi-Quantum Channel Nano-FETs

  2013cites this paper
• A Survey on Coping with the State Space Explosion Problem in Model Checking

  2013cites this paper
• A systematic verification of behavioral consistency between FBD design and ANSI-C implementation using HW-CBMC

  2013cites this paper
• SQAF-DS: A Software Quality Assessment Framework for Dependable Systems

  2013cites this paper
• Automatized high-level evaluation of security properties for RTL hardware designs

  2013cites this paper
• Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns

  2013influential citation
• Efficient handling of obligation constraints in synthesis from omega-regular specifications

  2013cites this paper
• A RESEARCH ON SEAMLESS PLATFORM CHANGE OF REACTOR PROTECTION SYSTEM FROM PLC TO FPGA

  2013cites this paper
• A safety-focused verification using software fault trees

  2012cites this paper
• Extracting unsatisfiable cores for LTL via temporal resolution

  2012cites this paper
• NuDE : Development Environment for Safety-Critical Software of Nuclear Power Plant

  2012cites this paper
• Specification and Verification of Concurrent Programs Through Refinements

  2012cites this paper
• TC 2 SMV : A CASE tool for Translating SMV Input Program from Test Cases Generated from State Chart Diagram in UML

  2012cites this paper
• Safety first: a two-stage algorithm for the synthesis of reactive systems

  2012cites this paper
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces

  2012cites this paper
• Formal Modeling and Verification of Operational Flight Program in a Small-Scale Unmanned Helicopter

  2012cites this paper
• Scalable formal verification of finite field arithmetic circuits using computer algebra techniques

  2012cites this paper
• Computing a Hierarchical Static Order for Decision Diagram-Based Representation from P/T Nets

  2012cites this paper
• An efficient refinement strategy exploiting component properties in a cegar process

  2012cites this paper
• Explicit or symbolic translation of linear temporal logic to automata

  2012cites this paper
• A polynomial time flow for implementing free-choice Petri-nets

  2012cites this paper
• Formal Model Extraction for Combinational Equivalence Checking

  2012influential citation
• Síntesis de circuitos digitales basada en la generación de funciones incompletas mediante el paradigma orientado a objetos con inferencia de tipos.

  2012cites this paper
• Linear Temporal Logic Symbolic Model Checking

  2011influential citation