Sciweavers

ATVA
2004
Springer
68views Hardware» more  ATVA 2004»
13 years 8 months ago
Theorem Proving Languages for Verification
Jean-Pierre Jouannaud
ATVA
2004
Springer
115views Hardware» more  ATVA 2004»
13 years 8 months ago
First-Order LTL Model Checking Using MDGs
In this paper, we describe a first-order linear time temporal logic (LTL) model checker based on multiway decision graphs (MDG). We developed a first-order temporal language, LMDG ...
Fang Wang, Sofiène Tahar, Otmane Aït M...
ATVA
2004
Springer
138views Hardware» more  ATVA 2004»
13 years 8 months ago
Providing Automated Verification in HOL Using MDGs
While model checking suffers from the state space explosion problem, theorem proving is quite tedious and impractical for verifying complex designs. In this work, we present a veri...
Tarek Mhamdi, Sofiène Tahar
ATVA
2004
Springer
67views Hardware» more  ATVA 2004»
13 years 9 months ago
Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets
Scott Little, David Walter, Nicholas Seegmiller, C...
ATVA
2004
Springer
106views Hardware» more  ATVA 2004»
13 years 9 months ago
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker
Serge Haddad, Jean-Michel Ilié, Kais Klai
ATVA
2004
Springer
146views Hardware» more  ATVA 2004»
13 years 9 months ago
A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata
Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata Akio Nakata, Tadaaki Tanimoto, Suguru Sasaki, Teruo Higashino Department of Information Networking, ...
Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teru...
ATVA
2004
Springer
76views Hardware» more  ATVA 2004»
13 years 9 months ago
A Temporal Assertion Extension to Verilog
Many circuit designs need to follow some temporal rules. However, it is hard to express and verify them in the past. Therefore, a temporal assertion extension to Verilog, called Te...
Kai-Hui Chang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Ku...
ATVA
2004
Springer
77views Hardware» more  ATVA 2004»
13 years 9 months ago
Localizing Errors in Counterexample with Iteratively Witness Searching
We propose a novel approach to locate errors in complex counterexample of safety property. Our approach measures the distance between two state transition traces with difference o...
ShengYu Shen, Ying Qin, Sikun Li
ATVA
2004
Springer
117views Hardware» more  ATVA 2004»
13 years 9 months ago
Component-Wise Instruction-Cache Behavior Prediction
nded Abstract – Oleg Parshin∗ Abdur Rakib† Stephan Thesing∗ Reinhard Wilhelm∗ The precise determination of worst-case execution times (WCETs) for programs is mostly bein...
Abdur Rakib, Oleg Parshin, Stephan Thesing, Reinha...