CHARME - researchr conference series publications

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 100 from 213

2005

An Analysis of SAT-Based Model Checking Techniques in an Industrial EnvironmentNina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan. charme 2005: 254-268 [doi]

Wired: Wire-Aware Circuit DesignEmil Axelsson, Koen Claessen, Mary Sheeran. charme 2005: 5-19 [doi]

Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization StrategiesJason Baumgartner, Hari Mony. charme 2005: 222-237 [doi]

Symbolic Partial Order Reduction for Rule Based Transition SystemsRitwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan. charme 2005: 332-335 [doi]

Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, ProceedingsDominique Borrione, Wolfgang J. Paul, editors, Volume 3725 of Lecture Notes in Computer Science, Springer, 2005.

Regular VacuityDoron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi. charme 2005: 191-206 [doi]

Is Formal Verification Bound to Remain a Junior Partner of Simulation?Wolfram Büttner. charme 2005: 1 [doi]

Verifying Quantitative Properties Using Bound FunctionsArindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar. charme 2005: 50-64 [doi]

Temporal Modalities for Concisely Capturing Timing DiagramsHana Chockler, Kathi Fisler. charme 2005: 176-190 [doi]

Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive PartitioningGianfranco Ciardo, Andy Jinqing Yu. charme 2005: 146-161 [doi]

On the Verification of Memory Management MechanismsIakov Dalinger, Mark A. Hillebrand, Wolfgang J. Paul. charme 2005: 301-316 [doi]

Towards the Pervasive Verification of Automotive SystemsThomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul. charme 2005: 3-4 [doi]

Verifying Timing Behavior by Abstract Interpretation of Executable CodeChristian Ferdinand, Reinhold Heckmann. charme 2005: 336-339 [doi]

Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and DatapathsMasahiro Fujita. charme 2005: 340-344 [doi]

Deadlock Prevention in the Æthereal ProtocolBiniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu. charme 2005: 345-348 [doi]

Acceleration of SAT-Based Iterative Property CheckingDaniel Große, Rolf Drechsler. charme 2005: 349-353 [doi]

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous ComputationOrna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster. charme 2005: 129-145 [doi]

How Thorough Is Thorough Enough?Arie Gurfinkel, Marsha Chechik. charme 2005: 65-80 [doi]

Verification Challenges in Configurable Processor Design with ASIP MeisterMasaharu Imai, Akira Kitajima. charme 2005: 2 [doi]

Error Detection Using BMC in a Parallel EnvironmentSubramanian K. Iyer, Jawahar Jain, Mukul R. Prasad, Debashis Sahoo, Thomas Sidle. charme 2005: 354-358 [doi]

Formalization of the DE2 LanguageWarren A. Hunt Jr., Erik Reeber. charme 2005: 20-34 [doi]

Formal Verification of SynchronizersTsachy Kapschitz, Ran Ginosar. charme 2005: 359-362 [doi]

Real-Time Model Checking Is Really SimpleLeslie Lamport. charme 2005: 162-175 [doi]

A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification ProblemsPanagiotis Manolios, Sudarshan K. Srinivasan. charme 2005: 363-366 [doi]

High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware DesignPetr Matousek, Ales Smrcka, Tomás Vojnar. charme 2005: 371-375 [doi]

Exploiting Constraints in Transformation-Based VerificationHari Mony, Jason Baumgartner, Adnan Aziz. charme 2005: 269-284 [doi]

Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral LogicKatell Morin-Allory, David Cachera. charme 2005: 376-379 [doi]

Counterexample Guided Invariant Discovery for Parameterized Cache Coherence VerificationSudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan. charme 2005: 317-331 [doi]

Efficient Symbolic Simulation via Dynamic Scheduling, Don t Caring, and Case SplittingViresh Paruthi, Christian Jacobi 0002, Kai Weber. charme 2005: 114-128 [doi]

Resolving Quartz OverloadingOliver Pell, Wayne Luk. charme 2005: 380-383 [doi]

A New SAT-Based Algorithm for Symbolic Trajectory EvaluationJan-Willem Roorda, Koen Claessen. charme 2005: 238-253 [doi]

FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT SolversMona Safar, M. Watheq El-Kharashi, Ashraf Salem. charme 2005: 384-387 [doi]

Predictive Reachability Using a Sample-Based ApproachDebashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson. charme 2005: 388-392 [doi]

Minimizing Counterexample of ACTL PropertyShengYu Shen, Ying Qin, Sikun Li. charme 2005: 393-397 [doi]

Improvements to the Implementation of Interpolant-Based Model CheckingJoão P. Marques Silva. charme 2005: 367-370 [doi]

Finding and Fixing FaultsStefan Staber, Barbara Jobstmann, Roderick Bloem. charme 2005: 35-49 [doi]

Data Refinement for Synchronous System Specification and ConstructionAlex Tsow, Steven D. Johnson. charme 2005: 398-401 [doi]

Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional UnitsMiroslav N. Velev. charme 2005: 97-113 [doi]

Automatic Generation of Hints for Symbolic TraversalDavid Ward, Fabio Somenzi. charme 2005: 207-221 [doi]

Identification and Counter Abstraction for Full Virtual SymmetryOu Wei, Arie Gurfinkel, Marsha Chechik. charme 2005: 285-300 [doi]

Introducing Abstractions via RewritingWilliam D. Young. charme 2005: 402-405 [doi]

A Case Study: Formal Verification of Processor Critical PropertiesEmmanuel Zarpas. charme 2005: 406-409 [doi]

Interleaved Invariant Checking with Dynamic AbstractionLiang Zhang, Mukul R. Prasad, Michael S. Hsiao. charme 2005: 81-96 [doi]

2003

A Hazards-Based Correctness Statement for Pipelined CircuitsMark Aagaard. charme 2003: 66-80 [doi]

Semi-formal Verification of Memory Systems by Symbolic SimulationHusam Abu-Haimed, Sergey Berezin, David L. Dill. charme 2003: 158-163 [doi]

Effcient Symbolic Model Checking of Software Using Partial Disjunctive PartitioningSharon Barner, Ishai Rabinovitz. charme 2003: 35-50 [doi]

A Programming Language Based Analysis of Operand ForwardingLennart Beringer. charme 2003: 270-276 [doi]

Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMPSven Beyer, Christian Jacobi 0002, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul. charme 2003: 51-65 [doi]

Convergence Testing in Term-Level Bounded Model CheckingRandal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia. charme 2003: 348-362 [doi]

Predicate Abstraction with Minimum PredicatesSagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman. charme 2003: 19-34 [doi]

Coverage Metrics for Formal VerificationHana Chockler, Orna Kupferman, Moshe Y. Vardi. charme 2003: 111-125 [doi]

Exact and Efficient Verification of Parameterized Cache Coherence ProtocolsE. Allen Emerson, Vineet Kahlon. charme 2003: 247-262 [doi]

On Combining Symmetry Reduction and Symbolic Representation for Efficient Model CheckingE. Allen Emerson, Thomas Wahl. charme 2003: 216-230 [doi]

Towards Diagrammability and Efficiency in Event Sequence LanguagesKathi Fisler. charme 2003: 185-199 [doi]

Efficient Distributed SAT and SAT-Based Distributed Bounded Model CheckingMalay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar. charme 2003: 334-347 [doi]

The PSL/Sugar Specification Language A Language for all SeasonsDaniel Geist. charme 2003: 3 [doi]

Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L Aquila, Italy, October 21-24, 2003, ProceedingsDaniel Geist, Enrico Tronci, editors, Volume 2860 of Lecture Notes in Computer Science, Springer, 2003.

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem ProvingMichael J. C. Gordon, Joe Hurd, Konrad Slind. charme 2003: 200-215 [doi]

On Complementing Nondeterministic Büchi AutomataSankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi. charme 2003: 96-110 [doi]

Reasoning about GSTE Assertion GraphsAlan J. Hu, Jeremy Casas, Jin Yang. charme 2003: 170-184 [doi]

Design and Implementation of an Abstract Interpreter for VHDLCharles Hymans. charme 2003: 263-269 [doi]

Improved Symbolic Verification Using Partitioning TechniquesSubramanian K. Iyer, Debashis Sahoo, Christian Stangier, Amit Narayan, Jawahar Jain. charme 2003: 410-424 [doi]

Linear and Nonlinear Arithmetic in ACL2Warren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore. charme 2003: 319-333 [doi]

The ROBDD Size of Simple CNF FormulasMichael Langberg, Amir Pnueli, Yoav Rodeh. charme 2003: 363-377 [doi]

On the Correctness of an Intrusion-Tolerant Group Communication ProtocolMohamed Layouni, Jozef Hooman, Sofiène Tahar. charme 2003: 231-246 [doi]

A Compositional Theory of Refinement for Branching TimePanagiotis Manolios. charme 2003: 304-318 [doi]

Inductive Assertions and Operational SemanticsJ. Strother Moore. charme 2003: 289-303 [doi]

Efficient Hybrid Reachability Analysis for Asynchronous Concurrent SystemsEnric Pastor, Marco A. Peña. charme 2003: 378-393 [doi]

Integrating RAM and Disk Based Verification within the Mur-phi VerifierGiuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli. charme 2003: 277-282 [doi]

Finite Horizon Analysis of Markov Chains with the Mur-phi VerifierGiuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli. charme 2003: 394-409 [doi]

What Is beyond the RTL Horizon for Microprocessor and System Design?Wolfgang Roesner. charme 2003: 1 [doi]

CTL May Be Ambiguous When Model Checking Moore MachinesCédric Roux, Emmanuelle Encrenaz. charme 2003: 164-169 [doi]

Constrained Symbolic Simulation with Mathematica and ACL2Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione. charme 2003: 150-157 [doi]

More Deterministic vs. Smaller Büchi Automata for Efficient LTL Model CheckingRoberto Sebastiani, Stefano Tonetta. charme 2003: 126-140 [doi]

Finding Regularity: Describing and Analysing Circuits That Are Not Quite RegularMary Sheeran. charme 2003: 4-18 [doi]

Design and Verification of CoreConnectTM IP Using EsterelSatnam Singh. charme 2003: 283-288 [doi]

The Charme of Abstract EntitiesFabio Somenzi. charme 2003: 2 [doi]

An Optimized Symbolic Bounded Model Checking EngineRachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer. charme 2003: 141-149 [doi]

Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SATYue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind. charme 2003: 81-95 [doi]

2001

A Framework for Microprocessor Correctness StatementsMark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones. charme 2001: 433-448 [doi]

Applications of Hierarchical Verification in Model CheckingRobert Beers, Rajnish Ghughal, Mark Aagaard. charme 2001: 40-57 [doi]

Formal Verification of the VAMP Floating Point UnitChristoph Berg, Christian Jacobi 0002. charme 2001: 325-339 [doi]

Multiclock EsterelGérard Berry, Ellen Sentovich. charme 2001: 110-125 [doi]

Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDsDirk Beyer. charme 2001: 86-91 [doi]

Using Abstract Specifications to Verify PowerPC:::TM::: Custom Memories by Symbolic Trajectory EvaluationJayanta Bhadra, Andrew K. Martin, Jacob A. Abraham, Magdy S. Abadir. charme 2001: 386-402 [doi]

Efficient Debugging in a Formal Verification EnvironmentFady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi. charme 2001: 275-292 [doi]

Induction-Oriented Formal Verification in Symmetric Interconnection NetworksEric Gascard, Laurence Pierre. charme 2001: 418-432 [doi]

View from the Fringe of the FringeSteven D. Johnson. charme 2001: 1-12 [doi]

Proof Engineering in the Large: Formal Verification of Pentium:::®::: 4 Floating-Point DividerRoope Kaivola, Katherine R. Kohatsu. charme 2001: 196-211 [doi]

Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on ChipXiaohua Kong, Radu Negulescu, Larry Weidong Ying. charme 2001: 370-385 [doi]

Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, ProceedingsTiziana Margaria, Thomas F. Melham, editors, Volume 2144 of Lecture Notes in Computer Science, Springer, 2001.

Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model CheckingKenneth L. McMillan. charme 2001: 179-195 [doi]

Verification of Basic Block Schedules Using RTL TransformationsRajesh Radhakrishnan, Elena Teica, Ranga Vemuri. charme 2001: 173-178 [doi]

Coverability Analysis Using Symbolic Model CheckingGil Ratsaby, Shmuel Ur, Yaron Wolfsthal. charme 2001: 155-160 [doi]

Formal Pipeline DesignTiberiu Seceleanu, Juha Plosila. charme 2001: 167-172 [doi]

A Specification Methodology by a Collection of Compact Properties as Applied to the Intel:::®::: Itanium:::TM::: Processor Bus ProtocolKanna Shimizu, David L. Dill, Ching-Tsun Chou. charme 2001: 340-354 [doi]

Deriving Real-Time Programs from Duration Calculus SpecificationsFrançois Siewe, Dang Van Hung. charme 2001: 92-97 [doi]

Pruning Techniques for the SAT-Based Bounded Model Checking ProblemOfer Strichman. charme 2001: 58-70 [doi]

Temporal Properties of Self-Timed RingsAnthony Winstanley, Mark R. Greenstreet. charme 2001: 140-154 [doi]

Reproducing Synchronization Bugs with Model CheckingKaren Yorav, Sagi Katz, Ron Kiper. charme 2001: 98-103 [doi]

Links

Filter by Year
OR AND NOT 1

Filter by Tag

[+]
OR AND NOT 1

Filter by Author

[+]
OR AND NOT 1

Filter by Top terms

[+]
OR AND NOT 1

CHARME (charme)

Viewing Publication 1 - 100 from 213

2005

2003

2001

Links

Filter by YearOR AND NOT 1

Filter by Tag [+]OR AND NOT 1

Filter by Author [+]OR AND NOT 1

Filter by Top terms [+]OR AND NOT 1

CHARME (charme)

Viewing Publication 1 - 100 from 213

2005

2003

2001

Filter by Year
OR AND NOT 1

Filter by Tag

[+]
OR AND NOT 1

Filter by Author

[+]
OR AND NOT 1

Filter by Top terms

[+]
OR AND NOT 1