Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
20 | Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
A Tutorial on Using PVS for Hardware Verification. |
TPCD |
1994 |
DBLP DOI BibTeX RDF |
|
20 | Jens Ulrik Skakkebæk, Natarajan Shankar |
Towards a Duration Calculus Proof Assistant in PVS. |
FTRTFT |
1994 |
DBLP DOI BibTeX RDF |
|
20 | John M. Rushby, Jens Ulrik Skakkebæk |
The PVS Verification System and PC/DC. |
FTRTFT |
1994 |
DBLP BibTeX RDF |
|
20 | Sam Owre, John M. Rushby, Natarajan Shankar |
PVS: A Prototype Verification System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
20 | Gebhard Greiter |
Zu zentralen Design-Entscheidungen beim Entwurf der Datenbank POINTE/PVS. |
BTW |
1987 |
DBLP DOI BibTeX RDF |
|
20 | Charles H. Applebaum, James G. Williams 0002 |
PVS - design for a practical verification system. |
ACM Annual Conference |
1984 |
DBLP DOI BibTeX RDF |
|
20 | Xiangyang Huang, Yan Peng |
A Vision Simulation Algorithm for Nonplayer Characters in Dynamic Scene. |
PACIIA (1) |
2008 |
DBLP DOI BibTeX RDF |
nonplayer character, visibility, PVS, dynamic scene |
20 | David R. Lester |
Real Number Calculations and Theorem Proving. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic |
20 | Peter Wonka, Michael Wimmer 0001, Kaichi Zhou, Stefan Maierhofer, Gerd Hesina, Alexander Reshetov |
Guided visibility sampling. |
ACM Trans. Graph. |
2006 |
DBLP DOI BibTeX RDF |
visibility sampling, visibility, PVS, occlusion culling |
20 | Samuli Laine |
A general algorithm for output-sensitive visibility preprocessing. |
SI3D |
2005 |
DBLP DOI BibTeX RDF |
visibility, PVS, occlusion culling |
20 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas |
Formal Verification of a Complex Pipelined Processor. |
Formal Methods Syst. Des. |
2003 |
DBLP DOI BibTeX RDF |
completion functions, formal verification, PVS, processor verification |
20 | Tommer Leyvand, Olga Sorkine, Daniel Cohen-Or |
Ray space factorization for from-region visibility. |
ACM Trans. Graph. |
2003 |
DBLP DOI BibTeX RDF |
line parameterization, visibility, hardware acceleration, PVS, occlusion culling, dual space |
20 | Timo Aaltonen, Pertti Kellomäki, Risto Pitkänen |
Specifying Cash-Point with DisCo. |
Formal Aspects Comput. |
2000 |
DBLP DOI BibTeX RDF |
DisCo, OO methods, Verification, Animation, Temporal logic, PVS |
20 | Frédo Durand, George Drettakis, Joëlle Thollot, Claude Puech |
Conservative visibility preprocessing using extended projections. |
SIGGRAPH |
2000 |
DBLP DOI BibTeX RDF |
PVS, occlusion culling, visibility determination |
20 | Murali Rangarajan, Perry Alexander, Nael B. Abu-Ghazaleh |
Using Automatable Proof Obligations for Component-Based Design Checking. |
ECBS |
1999 |
DBLP DOI BibTeX RDF |
Design Checking, Formal Verification, PVS, Compositional Analysis |
19 | Issa Traoré, Demissie B. Aredo |
Enhancing Structured Review with Model-Based Verification. |
IEEE Trans. Software Eng. |
2004 |
DBLP DOI BibTeX RDF |
Structured review, prototype verification system (PVS), model-based verification, UML, formal methods, OCL, validation and verification |
11 | Alex A. Aravind, Wim H. Hesselink |
A queue based mutual exclusion algorithm. |
Acta Informatica |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Hendrik Tews, Marcus Völp, Tjark Weber |
Formal Memory Models for the Verification of Low-Level Operating-System Code. |
J. Autom. Reason. |
2009 |
DBLP DOI BibTeX RDF |
Micro-hypervisor, Memory-mapped devices, Formal verification, Virtual memory, Operating-system kernel |
11 | Ingo Feinerer, Gernot Salzer |
A comparison of tools for teaching formal software verification. |
Formal Aspects Comput. |
2009 |
DBLP DOI BibTeX RDF |
Formal software verification, Frege Program Prover, Key system, Perfect developer, Prototype verification system |
11 | Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky |
Declarative Network Verification. |
PADL |
2009 |
DBLP DOI BibTeX RDF |
network protocol verification, theorem proving, domain-specific languages, Declarative networking |
11 | Cinzia Bernardeschi, Paolo Masci 0001, Holger Pfeifer |
Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios. |
SSS |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Alwyn Goodloe, César A. Muñoz |
Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle. |
FMICS |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Marieke Huisman, Alejandro Tamalet |
A Formal Connection between Security Automata and JML Annotations. |
FASE |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Marcus Völp, Claude-Joachim Hamann, Hermann Härtig |
Avoiding timing channels in fixed-priority schedulers. |
AsiaCCS |
2008 |
DBLP DOI BibTeX RDF |
security, real-time, information flow, fixed-priority scheduling, noninterference |
11 | Susumu Nishimura |
Safe Modification of Pointer Programs in Refinement Calculus. |
MPC |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Cezary Kaliszyk, Freek Wiedijk |
Merging Procedural and Declarative Proof. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Chanyang Joo, Soojae Kim, Kwangsub Yoon |
A low-power 12-bit 80MHz CMOS DAC using pseudo-segmentation. |
ACM Great Lakes Symposium on VLSI |
2008 |
DBLP DOI BibTeX RDF |
binary decoder, pseudo-segmentation, swing reduced driver, low power, DAC |
11 | Youngsik Kim, Nazanin Mansouri |
Automated formal verification of scheduling with speculative code motions. |
ACM Great Lakes Symposium on VLSI |
2008 |
DBLP DOI BibTeX RDF |
formal verification, high level synthesis, automated theorem-proving, speculation |
11 | Amir Pnueli, Yaniv Sa'ar |
All You Need Is Compassion. |
VMCAI |
2008 |
DBLP DOI BibTeX RDF |
|
11 | K. Mani Chandy, Sayan Mitra, Concetta Pilotto |
Convergence Verification: From Shared Memory to Partially Synchronous Systems. |
FORMATS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Yiheng Zhang, Heang-Ping Chan, Mitchell M. Goodsitt, Andrea Schmitz, Jeffrey W. Eberhard, Bernhard E. H. Claus |
Investigation of Different PV Distributions in Digital Breast Tomosynthesis (DBT) Mammography. |
Digital Mammography / IWDM |
2008 |
DBLP DOI BibTeX RDF |
Digital Breast Tomosynthesis (DBT) Mammography, distributions of projection-view (PV) images, simultaneous algebraic reconstruction technique (SART) |
11 | Bernd Becker 0001, Christian Dax, Jochen Eisinger, Felix Klaedtke |
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Bruno Dutertre |
Formal Modeling and Analysis of the Modbus Protocol. |
Critical Infrastructure Protection |
2007 |
DBLP DOI BibTeX RDF |
Modbus, modeling, formal methods, test-case generation |
11 | José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina |
A Formally Verified Prover for the ALC Description Logic. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Tonny Kurniadi Satyananda, Danhyung Lee, Sungwon Kang |
Formal Verification of Consistency between Feature Model and Software Architecture in Software Product Line. |
ICSEA |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Myeong-Eun Hwang, Tamer Cakici, Kaushik Roy 0001 |
Interactive presentation: Process tolerant beta-ratio modulation for ultra-dynamic voltage scaling. |
DATE |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Tonny Kurniadi Satyananda, Danhyung Lee, Sungwon Kang |
A Formal Approach to Verify Mapping Relation in a Software Product Line. |
CIT |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Ralph-Johan Back, Johannes Eriksson, Magnus Myreen |
Testing and Verifying Invariant Based Programs in the SOCOS Environment. |
TAP |
2007 |
DBLP DOI BibTeX RDF |
Invariant based programming, static program verification, state charts, verification conditions |
11 | Marc Daumas, David R. Lester |
Stochastic Formal Methods: An Application to Accuracy of Numeric Software. |
HICSS |
2007 |
DBLP DOI BibTeX RDF |
|
11 | J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro |
Verification of Program Properties Using Different Theorem Provers: A Case Study. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Amjad Gawanmeh, Sofiène Tahar |
Rank Theorems for Forward Secrecy in Group Key Management Protocols. |
AINA Workshops (1) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Robert Colvin, Lindsay Groves |
A Scalable Lock-Free Stack Algorithm and its Verification. |
SEFM |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Wim H. Hesselink |
Refinement verification of the lazy caching algorithm. |
Acta Informatica |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sven Beyer, Christian Jacobi 0002, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul |
Putting it all together - Formal verification of the VAMP. |
Int. J. Softw. Tools Technol. Transf. |
2006 |
DBLP DOI BibTeX RDF |
Complete microprocessor verification, Tomasulo scheduler, Cache memory interface, Model checking, Formal methods, Theorem proving, Floating point unit |
11 | Jozef Hooman, Mark van der Zwaag |
A semantics of communicating reactive objects with timing. |
Int. J. Softw. Tools Technol. Transf. |
2006 |
DBLP DOI BibTeX RDF |
UML, Real-time, Formal methods, Theorem proving, Formal semantics |
11 | Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir |
Formal Verification of a Lazy Concurrent List-Based Set Algorithm. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Katell Morin-Allory, Dominique Borrione |
Proven correct monitors from PSL specifications. |
DATE |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Viorel Preoteasa |
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Robert L. Constable, Wojciech Moczydlowski |
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Benjamin Werner |
On the Strength of Proof-Irrelevant Type Theories. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Xiang Yin 0001 |
The echo approach to formal verification. |
ICSE |
2006 |
DBLP DOI BibTeX RDF |
formal specification, formal verification |
11 | Ralph-Johan Back, Viorel Preoteasa |
An algebraic treatment of procedure refinement to support mechanical verification. |
Formal Aspects Comput. |
2005 |
DBLP DOI BibTeX RDF |
Semantics, Refinement, Hoare logic, Recursive procedures, Mechanical verification |
11 | Yves Bertot, Laurent Théry |
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Rohit Gheyi, Tiago Massoni |
Formal refactorings for object models. |
OOPSLA Companion |
2005 |
DBLP DOI BibTeX RDF |
theorem proving, object models, model refactoring |
11 | David A. Naumann |
Verifying a Secure Information Flow Analyzer. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
11 | César A. Muñoz, David R. Lester |
Real Number Calculations and Theorem Proving. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Bart Jacobs 0001, Wolter Pieters, Martijn Warnier |
Statically checking confidentiality via dynamic labels. |
WITS |
2005 |
DBLP DOI BibTeX RDF |
(Higher Order) theorem proving, formal verification, static analysis, abstract interpretation, confidentiality |
11 | Alessandro Armando, Luca Compagna, Silvio Ranise |
Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. |
Mechanizing Mathematical Reasoning |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Nikhil Kikkeri, Peter-Michael Seidel |
Formal Verification of Parametric Multiplicative Division Implementations. |
ICCD |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Youngsik Kim, Parija Sule, Nazanin Mansouri |
Exploiting PSL standard assertions in a theorem-proving-based verification environment. |
ACM Great Lakes Symposium on VLSI |
2005 |
DBLP DOI BibTeX RDF |
assertion-based design, modeling, verification, theorem-proving, formal semantics, PSL |
11 | John Eberhard, Anand Tripathi |
Object-Based Commutativity Analysis for Real-Time Applications. |
WORDS |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Rohit Gheyi, Tiago Massoni, Paulo Borba |
A rigorous approach for proving model refactorings. |
ASE |
2005 |
DBLP DOI BibTeX RDF |
theorem proving, model refactoring |
11 | Robert Colvin, Lindsay Groves |
Formal Verification of an Array-Based Nonblocking Queue. |
ICECCS |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Carlo A. Furia, Matteo Rossi 0001, Dino Mandrioli, Angelo Morzenti |
Automated Compositional Proofs for Real-Time Systems. |
FASE |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Tamarah Arons |
Verification of an Advanced mips-Type Out-of-Order Execution Algorithm. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Hui Gao, Wim H. Hesselink |
A Formal Reduction for Lock-Free Parallel Algorithms. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Chris George |
Tutorial on the RAISE Language, Method and Tools. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Ali Hamie |
Translating the Object Constraint Language into the Java Modelling Language. |
SAC |
2004 |
DBLP DOI BibTeX RDF |
UML, constraints, reasoning, OCL, JML |
11 | Wan J. Fokkink, Jan Friso Groote, Jun Pang 0001, Bahareh Badban, Jaco van de Pol |
Verifying a Sliding Window Protocol in µCRL. |
AMAST |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Lu Yan |
Formal Verification of a Ubiquitous Hardware Component. |
ICESS |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Carmen Graciani Díaz, Mario J. Pérez-Jiménez |
Using Automated Reasoning Systems on Molecular Computing. |
DNA |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Hui Gao, Jan Friso Groote, Wim H. Hesselink |
Almost Wait-Free Resizable Hashtable. |
IPDPS |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar |
The ICS Decision Procedures for Embedded Deduction. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Ajay Chander, Drew Dean, John C. Mitchell |
A Distributed High Assurance Reference Monitor. |
ISC |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Byoung-Ju Yun, Si-Woong Lee, Jae-Soo Cho, Jae-Gark Choi, Hyun Soo Kang |
A New Vertex Selection Scheme Using Curvature Information. |
KES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Nikhil Kikkeri, Peter-Michael Seidel |
Formal Hardware Verification based on Signal Correlation Properties. |
ICCD |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Jaemyung Cho, Junbeom Yoo, Sung Deok Cha |
NuEditor - A Tool Suite for Specification and Verification of NuSCR. |
SERA |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Simon Doherty, Lindsay Groves, Victor Luchangco, Mark Moir |
Formal Verification of a Practical Lock-Free Queue Algorithm. |
FORTE |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Vu Ha, Murali Rangarajan, Darren D. Cofer, Harald Rueß, Bruno Dutertre |
Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report. |
ICSE |
2004 |
DBLP DOI BibTeX RDF |
|
11 | K. Gopinath, Anil K. Pugalia, K. V. M. Naidu |
Formal Proof of Impossibility of Reliability in Crashing Protocols. |
IWDC |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Naga K. Govindaraju, Brandon Lloyd, Sung-Eui Yoon, Avneesh Sud, Dinesh Manocha |
Interactive shadow generation in complex environments. |
ACM Trans. Graph. |
2003 |
DBLP DOI BibTeX RDF |
level-of-detail, visibility, shadows, parallel rendering, interactive display |
11 | Christoph Sprenger 0001, Krzysztof Worytkiewicz |
A Verification Methodology for Infinite-State Message Passing Systems. |
MEMOCODE |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl |
Proving the Shalls. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Marcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum |
Taking Alloy to the Movies. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Mohamed Layouni, Jozef Hooman, Sofiène Tahar |
On the Correctness of an Intrusion-Tolerant Group Communication Protocol. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Sven Beyer, Christian Jacobi 0002, Daniel Kroening, Dirk Leinenbach, Wolfgang J. Paul |
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Suad Alagic, Jeremy Logan |
Consistency of Java Transactions. |
DBPL |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Zhi Zheng 0007, Tony K. Y. Chan |
Optimized Neighbour Prefetch and Cache for Client-server Based Walkthrough. |
CW |
2003 |
DBLP DOI BibTeX RDF |
|
11 | Murali Rangarajan, Kshama Jambhekar, Amitvikram Rajkhowa, Perry Alexander |
VSPEC and Its Integrated Tool Suite. |
ECBS |
2002 |
DBLP DOI BibTeX RDF |
VSPEC, Constraints Verification, Requirements Analysis, Functional Verification, Test Vector Generation |
11 | Jozef Hooman, Jaco van de Pol |
Formal verification of replication on a distributed data space architecture. |
SAC |
2002 |
DBLP DOI BibTeX RDF |
data space architecture, model-checking, formal verification, coordination, theorem proving |
11 | Cees-Bart Breunesse, Bart Jacobs 0001, Joachim van den Berg |
Specifying and Verifying a Decimal Representation in Java for Smart Cards. |
AMAST |
2002 |
DBLP DOI BibTeX RDF |
|
11 | Vlad Rusu |
Verification Using Test Generation Techniques. |
FME |
2002 |
DBLP DOI BibTeX RDF |
electronic purse, Formal verification, conformance testing |
11 | Ashish Tiwari 0001, Gaurav Khanna 0001 |
Series of Abstractions for Hybrid Automata. |
HSCC |
2002 |
DBLP DOI BibTeX RDF |
|
11 | Jozef Hooman, Jaco van de Pol |
Equivalent Semantic Models for a Distributed Dataspace Architecture. |
FMCO |
2002 |
DBLP DOI BibTeX RDF |
|
11 | Silvio Ranise |
Combining Generic and Domain Specific Reasoning by Using Contexts. |
AISC |
2002 |
DBLP DOI BibTeX RDF |
|
11 | Milos Besta, Frank A. Stomp |
Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm. |
ICECCS |
2002 |
DBLP DOI BibTeX RDF |
|
11 | Steven Shapiro, Yves Lespérance, Hector J. Levesque |
The cognitive agents specification language and verification environment for multiagent systems. |
AAMAS |
2002 |
DBLP DOI BibTeX RDF |
agent specification languages, theorem proving, proof assistants, verification tools |
11 | Marieke Huisman, Bart Jacobs 0001, Joachim van den Berg |
A case study in class library verification: Java's vector class. |
Int. J. Softw. Tools Technol. Transf. |
2001 |
DBLP DOI BibTeX RDF |
Java, Specification, Program verification, Invariant |
11 | Angelo Gargantini, Angelo Morzenti |
Automated deductive requirements analysis of critical systems. |
ACM Trans. Softw. Eng. Methodol. |
2001 |
DBLP DOI BibTeX RDF |
finite variability, temporal logic, theorem proving, hybrid systems, state-transition systems |
11 | Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar |
ICS: Integrated Canonizer and Solver. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|