24 papers:
CAV-2015-MasciOZJCT #human-computer- PVSio-web 2.0: Joining PVS to HCI (PM, PO, YZ, PLJ, PC, HWT), pp. 470–478.
FASE-2014-MasciZJCT #user interface #using #verification- Formal Verification of Medical Device User Interfaces Using PVS (PM, YZ, PLJ, PC, HWT), pp. 200–214.
FM-2014-DenmanM #automation #proving- Automated Real Proving in PVS via MetiTarski (WD, CAM), pp. 194–199.
TACAS-2007-FriasPM #alloy #analysis #specification #verification- Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications (MFF, CLP, MMM), pp. 587–601.
- FM-2006-UmenoL #automaton #case study #protocol #proving #safety #theorem proving #using
- Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study (SU, NAL), pp. 64–80.
SEFM-2006-KanadeSK #compilation #framework #optimisation #validation- A PVS Based Framework for Validating Compiler Optimizations (AK, AS, UPK), pp. 108–117.
- SEFM-2006-Rushby06a #automation #formal method #named #tutorial
- Tutorial: Automated Formal Methods with PVS, SAL, and Yices (JMR), p. 262.
SEKE-2006-LeeDSG #approach #modelling #verification- A PVS Approach to Verifying ORA-SS Data Models (SUJL, GD, JS, LG), pp. 126–131.
IFM-2005-WeiH #csp- Embedding the Stable Failures Model of CSP in PVS (KW, JH), pp. 246–265.
- TACAS-2002-KimSC #functional #requirements #specification #using #verification
- Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS (TK, DWJSC, SDC), pp. 205–220.
- FASE-2001-PaigeO #consistency #metamodelling
- Metamodelling and Conformance Checking with PVS (RFP, JSO), pp. 2–16.
- CAV-2000-OwreR
- Integrating WS1S with PVS (SO, HR), pp. 548–551.
- TACAS-1999-BastenH #algebra #process
- Process Algebra in PVS (TB, JH), pp. 270–284.
- FM-v2-1999-Droschl #data access #requirements #using
- Analyzing the Requirements of an Access Control Using VDMTools and PVS (GD), p. 1870.
- FM-v2-1999-LevyT #approach #education
- A PVS-Based Approach for Teaching Constructing Correct Iterations (ML, LT), pp. 1859–1860.
- FM-1998-OwreRSS #case study #experience #named
- PVS: An Experience Report (SO, JMR, NS, DWJSC), pp. 338–345.
ASE-1997-MaharajB #on the #refinement #specification #verification- On the Verification of VDM Specification and Refinement with PVS (SM, JB), p. 280–?.
- TACAS-1997-OwreRS #integration #model checking
- Integration in PVS: Tables, Types, and Model Checking (SO, JMR, NS), pp. 366–383.
- FME-1997-Kellomaki #using #verification
- Verification of Reactive Systems Using DisCo and PVS (PK), pp. 589–604.
- FME-1997-Stringer-CalvertSW #case study #refinement #using
- Using PVS to Prove a Z Refinement: A Case Study (DWJSC, SS, IW), pp. 573–588.
- CAV-1997-GrafS #graph
- Construction of Abstract State Graphs with PVS (SG, HS), pp. 72–83.
- CAV-1996-OwreRRSS #model checking #named #proving #specification
- PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
- CAV-1993-Shankar #realtime #using #verification
- Verification of Real-Time Systems Using PVS (NS), pp. 280–291.
CADE-1992-OwreRS #named #prototype #verification- PVS: A Prototype Verification System (SO, JMR, NS), pp. 748–752.
