Search results for "PVS"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
112	Savi Maharaj, Juan Bicarregui	On the Verification of VDM Specification and Refinement with PVS.	ASE	1997	DBLP DOI BibTeX RDF	VDM specification, VDM formal method, PVS theorem prover, VDM-SL specification translation, PVS specification language, transparent translation methods, specification type-checking, nontrivial validation conditions, abstract specification, shallow embedding technique, verification, formal specification, proof rules
109	Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene	Using TAME to prove invariants of automata models: Two case studies.	FMSP	2000	DBLP DOI BibTeX RDF	software requirements analysis, Software engineering, verification, formal methods, theorem proving
94	Youngjin Cho, Younghyun Kim 0001, Naehyuck Chang	PVS: passive voltage scaling for wireless sensor networks.	ISLPED	2007	DBLP DOI BibTeX RDF	embedded system, low-power, wireless, DVS, PVS, sensor node
83	Jin Song Dong, Yuzhang Feng, Yuan-Fang Li	Verifying OWL and ORL Ontologies in PVS.	ICTAC	2004	DBLP DOI BibTeX RDF	ORL, Semantic Web, OWL, reasoning, PVS
72	Gwen Salaün, J. Christian Attiogbé	Formalising an Integrated Language in PVS.	ICFEM	2003	DBLP DOI BibTeX RDF	Formal Method Integration, Equivalence Proof, Embedding, Process Algebra, Algebraic Specifications, PVS
72	Jean-Paul Bodeveix, Mamoun Filali	Type Synthesis in B and the Translation of B to PVS.	ZB	2002	DBLP DOI BibTeX RDF	semantics, type theory, PVS, logical frameworks, B
66	Heang-Ping Chan, Jun Wei 0002, Yiheng Zhang, Berkman Sahiner, Lubomir M. Hadjiiski, Mark A. Helvie	Detection of Masses in Digital Breast Tomosynthesis Mammography: Effects of the Number of Projection Views and Dose.	Digital Mammography / IWDM	2008	DBLP DOI BibTeX RDF	computer-aided detection, mass, Digital breast tomosynthesis
64	Richard F. Paige, Jonathan S. Ostroff	Metamodelling and Conformance Checking with PVS.	FASE	2001	DBLP DOI BibTeX RDF
64	Angelo Gargantini, Elvinia Riccobene	Encoding Abstract State Machines in PVS.	Abstract State Machines	2000	DBLP DOI BibTeX RDF
63	Chunqing Chen, Jin Song Dong, Jun Sun 0001	A verification system for timed interval calculus.	ICSE	2008	DBLP DOI BibTeX RDF	real-time systems, theorem proving, specification language, pvs
63	Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag	Deductive Verification of UML Models in TLPVS.	UML	2004	DBLP DOI BibTeX RDF	Deductive Verification, UML, Semantics, Formal Verification, Temporal Logic, State Machines, PVS
63	Jonathan Ford, Ian A. Mason	Formal Foundations of Operational Semantics.	High. Order Symb. Comput.	2003	DBLP DOI BibTeX RDF	contexts, theorem proving, operational semantics, PVS, calculus
61	Mats Per Erik Heimdahl, Barbara J. Czerny	Using PVS to analyze hierarchical state-based requirements for completeness and consistency.	HASE	1996	DBLP DOI BibTeX RDF	hierarchical state based requirements specifications, input sequence, analysis procedures, large real world requirements specification, hierarchical state based language, Requirements State Machine Language, Prototype Verification System, theorem proving component, spurious error reports, formal specifications, robustness, consistency, program verification, completeness, Binary Decision Diagrams, BDDs, PVS, interactive environment, formal proofs, RSML
61	Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke	Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.	IEEE Trans. Software Eng.	1995	DBLP DOI BibTeX RDF	verification systems, fault tolerance, formal specification, formal methods, theorem proving, clock synchronization, PVS, Byzantine agreement, hardware verification, flight control
55	Fábio O. Moreira, João Comba, Carla Maria Dal Sasso Freitas	Smart Visible Sets for Networked Virtual Environments.	SIBGRAPI	2002	DBLP DOI BibTeX RDF
53	Sam Owre, Natarajan Shankar	A Brief Overview of PVS.	TPHOLs	2008	DBLP DOI BibTeX RDF
53	Shinya Umeno, Nancy A. Lynch	Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study.	FM	2006	DBLP DOI BibTeX RDF
53	Myla Archer	Making PVS do what you want.	MEMOCODE	2005	DBLP DOI BibTeX RDF
53	Herwig Lejsek	A case-study of scoring schemes for the PvS-index.	CVDB	2005	DBLP DOI BibTeX RDF
53	Sanjai Rayadurgam, Anjali Joshi, Mats Per Erik Heimdahl	Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language.	ICFEM	2003	DBLP DOI BibTeX RDF
53	David R. Lester	Using PVS to Validate the Inverse Trigonometric Functions of an Exact Arithmetic.	Numerical Software with Result Verification	2003	DBLP DOI BibTeX RDF
53	Michel Allemand, Jean-Claude Royer	Mixed Formal Specifications with PVS.	IPDPS	2002	DBLP DOI BibTeX RDF
53	Erika Ábrahám-Mumm, Ulrich Hannemann, Martin Steffen	Assertion-Based Analysis of Hybrid Systems with PVS.	EUROCAST	2001	DBLP DOI BibTeX RDF	deductive methods, machine-assisted verification, hybrid systems
53	Myla Archer, Constance L. Heitmeyer	Human-Style Theorem Proving Using PVS.	TPHOLs	1997	DBLP DOI BibTeX RDF
53	Natarajan Shankar	Verification of Real-Time Systems Using PVS.	CAV	1993	DBLP DOI BibTeX RDF
52	Demissie B. Aredo, Olaf Owe	Model-Based Verification in the Development of Dependable Systems.	ITCC (2)	2005	DBLP DOI BibTeX RDF	Model-based Verification, Model-checking, UML, Formal Methods, PVS, Dependable System
52	Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir	Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs.	LOPSTR	2004	DBLP DOI BibTeX RDF	Addition of faulttolerance, Fault-tolerance, Program transformation, Theorem proving, Program synthesis, PVS, Mechanical verification
50	Changlong Zhu, Rasha Morsi	Formal specification of FFHMIPv6 using PVS.	SpringSim	2009	DBLP BibTeX RDF	FFHMIPv6 packets, formal methods, handover, PVS
50	Cinzia Bernardeschi, Paolo Masci 0001, Holger Pfeifer	Early Prototyping of Wireless Sensor Network Algorithms in PVS.	SAFECOMP	2008	DBLP DOI BibTeX RDF	WSN algorithms, simulation, PVS
50	Neil Evans, Steve A. Schneider	Analysing Time Dependent Security Properties in CSP Using PVS.	ESORICS	2000	DBLP DOI BibTeX RDF	Authentication Protocol Verification, Timed Behaviour, CSP, Automated Theorem Proving, PVS
50	John M. Rushby, Sam Owre, Natarajan Shankar	Subtypes for Specifications: Predicate Subtyping in PVS.	IEEE Trans. Software Eng.	1998	DBLP DOI BibTeX RDF	typechecking, Formal methods, consistency, type systems, specification languages, subtypes, PVS
44	Kai Lampka, Markus Siegle	Analysis of Markov reward models using zero-suppressed multi-terminal BDDs.	VALUETOOLS	2006	DBLP DOI BibTeX RDF	performance evaluation tool, symbolic data structure, Markov chain, discrete event systems, numerical solution
44	Suad Alagic, Mark Royer, David Briggs	Verification Theories for XML Schema.	BNCOD	2006	DBLP DOI BibTeX RDF
44	Timothy Roden, Ian Parberry	Portholes and planes: faster dynamic evaluation of potentially visible sets.	Comput. Entertain.	2005	DBLP DOI BibTeX RDF	portal rendering, visibility, occlusion culling
44	Chang Wook Ahn, Ki Pyo Kim, Rudrapatna S. Ramakrishna	A Memory-Efficient Elitist Genetic Algorithm.	PPAM	2003	DBLP DOI BibTeX RDF
44	Sreeranga P. Rajan, Natarajan Shankar, Mandayam K. Srivas	Industrial Strength Formal Verification Techniques for Hardware Designs.	VLSI Design	1997	DBLP DOI BibTeX RDF
44	Harald Rueß, Natarajan Shankar, Mandayam K. Srivas	Modular Verification of SRT Division.	CAV	1996	DBLP DOI BibTeX RDF
42	Rob Verhoeven, Francien Dechesne	Verifying Multi-party Authentication Using Rank Functions and PVS.	Formal Aspects in Security and Trust	2008	DBLP DOI BibTeX RDF
42	Scott Uk-Jin Lee, Jing Sun 0002, Gillian Dobbie, Lindsay Groves	Verifying Semistructured Data Normalization Using PVS.	ICECCS	2008	DBLP DOI BibTeX RDF
42	Judi Romijn, Wieger Wesselink, Arjan J. Mooij	Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS.	ATVA	2007	DBLP DOI BibTeX RDF
42	Marcelo F. Frias, Carlos López Pombo, Mariano M. Moscato	Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications.	TACAS	2007	DBLP DOI BibTeX RDF
42	Bart Jacobs 0001, John M. Rushby	PVS.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
42	John M. Rushby	Tutorial: Automated Formal Methods with PVS, SAL, and Yices.	SEFM	2006	DBLP DOI BibTeX RDF
42	Kun Wei, James Heather	Embedding the Stable Failures Model of CSP in PVS.	IFM	2005	DBLP DOI BibTeX RDF	CSP, deadlock, determinism, liveness, theorem prover
42	Taeho Kim, David W. J. Stringer-Calvert, Sung Deok Cha	Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS.	TACAS	2002	DBLP DOI BibTeX RDF
42	Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre	Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS.	TPHOLs	2001	DBLP DOI BibTeX RDF
42	Erika Ábrahám-Mumm, Martin Steffen, Ulrich Hannemann	Verification of Hybrid Systems: Formalization and Proof Rules in PVS.	ICECCS	2001	DBLP DOI BibTeX RDF	deductive methods, machine-assisted verification, hybrid systems
42	Cécile Canovas-Dumas, Paul Caspi	A PVS Proof Obligation Generator for Lustre Programs.	LPAR	2000	DBLP DOI BibTeX RDF
42	Hanne Gottliebsen	Transcendental Functions and Continuity Checking in PVS.	TPHOLs	2000	DBLP DOI BibTeX RDF
42	Twan Basten, Jozef Hooman	Process Algebra in PVS.	TACAS	1999	DBLP DOI BibTeX RDF
42	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
42	Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert	PVS: An Experience Report.	FM-Trends	1998	DBLP DOI BibTeX RDF
42	Susanne Graf, Hassen Saïdi	Construction of Abstract State Graphs with PVS.	CAV	1997	DBLP DOI BibTeX RDF	state graph exploration, theorem proving, abstract interpretation
42	Bruno Dutertre, Steve A. Schneider	Using a PVS Embedding of CSP to Verify Authentication Protocols.	TPHOLs	1997	DBLP DOI BibTeX RDF
42	David W. J. Stringer-Calvert, Susan Stepney, Ian Wand	Using PVS to Prove a Z Refinement: A Case Study.	FME	1997	DBLP DOI BibTeX RDF
41	Bart Jacobs 0001, Sjaak Smetsers, Ronny Wichers Schreur	Code-carrying theories.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Compression, Code generation, Functional languages, Unification, PVS, Proof assistants
41	Chunqing Chen, Jin Song Dong, Jun Sun 0001	Machine-Assisted Proof Support for Validation Beyond Simulink.	ICFEM	2007	DBLP DOI BibTeX RDF	Formal Verification, PVS, Simulink, Real-Time Specifications
41	Lee Pike	A Note on Inconsistent Axioms in Rushby's "Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms'.	IEEE Trans. Software Eng.	2006	DBLP DOI BibTeX RDF	time-triggered algorithms, Formal methods, formal verification, PVS, synchronous systems
41	Marcelo Glusman, Shmuel Katz	A Mechanized Proof Environment for the Convenient Computations Proof Method.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	convenient computations, proof environment, deductive theorem proving, formal verification, PVS
41	Michael Backes 0001, Christian Jacobi 0002	Cryptographically Sound and Machine-Assisted Verification of Security Protocols.	STACS	2003	DBLP DOI BibTeX RDF	verification, cryptography, semantics, specification, PVS, simulatability
41	Michael Backes 0001, Christian Jacobi 0002, Birgit Pfitzmann	Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation.	FME	2002	DBLP DOI BibTeX RDF	security, cryptography, formal verification, PVS, simulatability
41	Vangalur S. Alagar, D. Muthiayen	Towards a mechanical verification of real-time reactive systems modeled in UML.	RTCSA	2000	DBLP DOI BibTeX RDF	Prototype Verification System, real-time systems, UML, Unified Modeling Language, formal specification, object-oriented programming, program verification, specification languages, PVS, notation, safety-critical applications, mechanical verification, real-time reactive systems, design analysis, object-based systems
41	Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry Alexander, Harold W. Carter	An Extensible Formal Framework for the Specification and Verification of an Optimistic Simulation Protocol.	HICSS	1999	DBLP DOI BibTeX RDF	Software Engineering, Theorem Proving, Parallel Discrete Event Simulation, PVS, Formal specification and verification
40	Hassen Saïdi, Susmit Jha, Tuhin Sahai	math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories.	CoRR	2023	DBLP DOI BibTeX RDF
40	Florent Kirchner, César A. Muñoz	PVS#: Streamlined Tacticals for PVS.	STRATEGIES@IJCAR	2006	DBLP DOI BibTeX RDF
40	Peter Mauruschat	Das Prozeßrechner-gestützte modulare Farbgrafiksystem PVS/VGS 1300 / The process control computer based colour graphics system PVS/VGS 1300.	Elektron. Rechenanlagen	1985	DBLP DOI BibTeX RDF
39	Qingguo Xu, Huaikou Miao	Manipulating Clocks in Timed Automata Using PVS.	SNPD	2009	DBLP DOI BibTeX RDF	clock manipulation, real-time system, Timed Automata, PVS
33	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
33	Neil Evans, Helen Treharne	Interactive tool support for CSP \|\| B consistency checking.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Formal method integration, Tool supported verification, Rely/guarantee techniques, CSP, B
33	Ajith K. John, Babita Sharma, A. K. Bhattacharjee, S. D. Dhodapkar, S. Ramesh 0001	Detection of Runtime Errors in MISRA C Programs: A Deductive Approach.	SAFECOMP	2007	DBLP DOI BibTeX RDF
33	Man Wang, Zhihui Du, Yinong Chen, Zhili Cheng	A SOA Based Pipeline System to Deal with Astronomy Telescope Data.	SOSE	2006	DBLP DOI BibTeX RDF	Pipeline Data Processing, Service-Oriented Architecture, Grid Middleware
33	Qing Wu, King To Ng, Shing-Chow Chan, Heung-Yeung Shum	On object-based compression for a class of dynamic image-based representations.	ICIP (3)	2005	DBLP DOI BibTeX RDF
33	Peter Frey, Radharamanan Radhakrishnan, Harold W. Carter, Philip A. Wilsey, Perry Alexander	A Formal Specification and Verification Framework for Time Warp-Based Parallel Simulation.	IEEE Trans. Software Eng.	2002	DBLP DOI BibTeX RDF	formal specification, formal verification, theorem proving, time warp, parallel discrete event simulation
33	Ben L. Di Vito	High-automation proofs for properties of requirements models.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Avionics software, Proof strategies, Formal methods, Theorem proving, Requirements analysis
33	Paul Z. Kolano	Proof Assistance for Real-Time Systems Using an Interactive Theorem Prover.	ARTS	1999	DBLP DOI BibTeX RDF
33	Ulrich Hensel, Marieke Huisman, Bart Jacobs 0001, Hendrik Tews	Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools.	ESOP	1998	DBLP DOI BibTeX RDF
33	Patrick Lincoln, John M. Rushby	The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model.	CAV	1993	DBLP DOI BibTeX RDF
31	Sayan Mitra, K. Mani Chandy	A Formalized Theory for Verifying Stability and Convergence of Automata in PVS.	TPHOLs	2008	DBLP DOI BibTeX RDF
31	Frits W. Vaandrager, Adriaan de Groot	Analysis of a biphase mark protocol with Uppaaland PVS.	Formal Aspects Comput.	2006	DBLP DOI BibTeX RDF	Biphase mark protocol, Model checking, Formal methods, Timed automata, Theorem provers
31	Mauricio Ayala-Rincón, Thomas Mailleux Santana	SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS.	SBCCI	2006	DBLP DOI BibTeX RDF
31	Aditya Kanade, Amitabha Sanyal, Uday P. Khedker	A PVS Based Framework for Validating Compiler Optimizations.	SEFM	2006	DBLP DOI BibTeX RDF
31	Bahareh Badban, Wan J. Fokkink, Jan Friso Groote, Jun Pang 0001, Jaco van de Pol	Verification of a sliding window protocol in µCRL and PVS.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	?CRL, Specification, Process algebra, Verification techniques, Sliding window protocols, Branching bisimulation
31	Arjan J. Mooij, Wieger Wesselink	Incremental Verification of Owicki/Gries Proof Outlines Using PVS.	ICFEM	2005	DBLP DOI BibTeX RDF
31	Néstor Cataño	Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS.	TPHOLs	2005	DBLP DOI BibTeX RDF
31	Hongping Lim, Dilsun Kirli Kaynar, Nancy A. Lynch, Sayan Mitra	Translating Timed I/O Automata Specifications for Theorem Proving in PVS.	FORMATS	2005	DBLP DOI BibTeX RDF
31	Weijiang Yu, Aloysius K. Mok	Formal Specification and Verification of Resource Bound Security Using PVS.	ISSS	2003	DBLP DOI BibTeX RDF
31	Amir Pnueli, Tamarah Arons	TLPVS: A PVS-Based LTL Verification System.	Verification: Theory and Practice	2003	DBLP DOI BibTeX RDF
31	Bart Jacobs 0001	Java's Integral Types in PVS.	FMOODS	2003	DBLP DOI BibTeX RDF
31	J. Christian Attiogbé	Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS.	ICFEM	2002	DBLP DOI BibTeX RDF
31	Pertti Kellomäki	A Structural Embedding of Ocsid in PVS.	TPHOLs	2001	DBLP DOI BibTeX RDF
31	Cindy Kong, Perry Alexander, Darryl D. Dieckman	Formal modeling of active network nodes using PVS.	FMSP	2000	DBLP DOI BibTeX RDF
31	Axel Dold	Software Development in PVS Using Generic Development Steps.	Generic Programming	1998	DBLP DOI BibTeX RDF	generic development steps, transformational software development, formal verification, mechanized theorem proving
31	Dang Van Hung	Modeling and Verification of Biphase Mark Protocolsin Duration Calculus Using PVS.	ACSD	1998	DBLP DOI BibTeX RDF	Biphase Mark Protocol, Theorem Prover, Duration Calculus
31	Pertti Kellomäki	Verification of Reactive Systems Using DisCo and PVS.	FME	1997	DBLP DOI BibTeX RDF
31	Jozef Hooman	Verifying Part of the ACCESS.bus Protocol Using PVS.	FSTTCS	1995	DBLP DOI BibTeX RDF
31	John M. Rushby, Mandayam K. Srivas	Using PVS to Prove Some Theorems Of David Parnas.	HUG	1993	DBLP DOI BibTeX RDF
31	David Briggs, Suad Alagic	Algebraic specification techniques for parametric types with logic-based constraints.	SAC	2009	DBLP DOI BibTeX RDF	parametric types, verification theories, assertions, PVS, JML
31	Chris George, Anne E. Haxthausen	Specification, proof, and model checking of the Mondex electronic purse using RAISE.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Verification, Formal methods, PVS, SAL, RAISE, Mondex
31	Leonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen	Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization.	FMICS	2007	DBLP DOI BibTeX RDF	simulation, verification, theorem proving, PVS, cyclic scheduling
31	Wan J. Fokkink, Jun Pang 0001, Jaco van de Pol	Cones and foci: A mechanical framework for protocol verification.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	Process algebra, PVS, Protocol verification, Branching bisimulation