Search results for "PVS"

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