Search results for "PVS"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
31	Christian Jacobi 0002, Christoph Berg	Formal Verification of the VAMP Floating Point Unit.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	IEEE standard 754, formal verification, theorem proving, PVS, floating point unit
31	Milos Besta, Frank A. Stomp	A Complete Mechanization of Correctness of a String-Preprocessing Algorithm.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	formal methods, pattern matching, theorem proving, PVS
31	Jan Friso Groote, François Monin, Jan Springintveld	A computer checked algebraic verification of a distributed summation algorithm.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	Distributed summation algorithm, Formal proof checking, Verification, Process algebra, PVS, CRL
31	Jei-Wen Teng, Yih-Kuen Tsay	Composing Temporal-Logic Specifications with Machine Assistance.	FME	2003	DBLP DOI BibTeX RDF	Assumption-Guarantee, Compositional Specification, Formal Correctness, Temporal Logic, Theorem Proving, Concurrent Systems, PVS, Compositional Verification, Component-Based Software
31	Vlad Rusu	Compositional Verification of an ATM Protocol.	FME	2003	DBLP DOI BibTeX RDF	SSCOP protocol, abstraction, theorem proving, Compositionality, PVS
31	Dmitri Chkliaev, Jozef Hooman, Peter van der Stok	Formal Modeling and Analysis of Atomic Commitment Protocols.	ICPADS	2000	DBLP DOI BibTeX RDF	real-time, formal specification, distributed databases, PVS, fault-tolerant systems, mechanical verification, atomic commitment protocols
31	John M. Rushby	Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms.	IEEE Trans. Software Eng.	1999	DBLP DOI BibTeX RDF	time-triggered algorithms, Formal methods, formal verification, PVS, synchronous systems
31	Tomohiro Yoneda, Yutaka Ohtsuka, Märt Saarepera	Verification of Parameterized Asynchronous Circuits: A Case Study.	ACSD	1998	DBLP DOI BibTeX RDF	parameterized asynchronous circuits, ACTL model checking, Formal verification, abstraction, PVS
30	Herwig Lejsek, Friðrik Heiðar Ásmundsson, Björn Þór Jónsson 0001, Laurent Amsaleg	Scalability of local image descriptors: a comparative study.	ACM Multimedia	2006	DBLP DOI BibTeX RDF	PvS-framework, median rank aggregation, scalability, high-dimensional indexing, local image descriptors
30	Padmanabhan Krishnan	Consistency checks for UML.	APSEC	2000	DBLP DOI BibTeX RDF	UML consistency checking, state predicates, PVS theorem prover, Prototype Verification System, partially specified systems, behavioural description, Unified Modeling Language, formal verification, theorem proving, specification languages, diagrams, computation history, UML diagrams, dynamic aspects
30	Simon Fowler 0002, Andy J. Wellings	Formal development of a real-time kernel.	RTSS	1997	DBLP DOI BibTeX RDF	formal development, simple real time operating system kernel, restricted Ada 95 tasking model, fixed priority real time systems, abstract specification, PVS proof system, computational model, RTL, operating system kernels
22	Simon Doherty, Mark Moir	Nonblocking Algorithms and Backward Simulation.	DISC	2009	DBLP DOI BibTeX RDF
22	Xiayong Hu, Mark Lawford, Alan Wassyng	Formal Verification of the Implementability of Timing Requirements.	FMICS	2008	DBLP DOI BibTeX RDF
22	André Luiz Galdino, César A. Muñoz, Mauricio Ayala-Rincón	Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm.	WoLLIC	2007	DBLP DOI BibTeX RDF
22	Jin Song Dong, Yuzhang Feng, Ho-fung Leung	A Verification Framework for Agent Knowledge.	ICFEM	2007	DBLP DOI BibTeX RDF
22	Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl	Proving the shalls.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF	Formal verification, Software requirements, Model-based development
22	Sylvie Boldo, César A. Muñoz	Provably faithful evaluation of polynomials.	SAC	2006	DBLP DOI BibTeX RDF	formal verification, floating-point, polynomial evaluation
22	Matthieu Sozeau	Subset Coercions in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
22	Kun Wei, James Heather	A Theorem-Proving Approach to Verification of Fair Non-repudiation Protocols.	Formal Aspects in Security and Trust	2006	DBLP DOI BibTeX RDF
22	Hui Gao, Jan Friso Groote, Wim H. Hesselink	Lock-free dynamic hash tables with open addressing.	Distributed Comput.	2005	DBLP DOI BibTeX RDF	Distributed algorithms, Wait-free, Lock-free, Hash tables
22	Marc Daumas, Guillaume Melquiond, César A. Muñoz	Guaranteed Proofs Using Interval Arithmetic.	IEEE Symposium on Computer Arithmetic	2005	DBLP DOI BibTeX RDF
22	Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang, Kees Goossens, Edwin Rijpkema, Andrei Radulescu	Deadlock Prevention in the Æthereal Protocol.	CHARME	2005	DBLP DOI BibTeX RDF
22	Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari 0001	SAL 2.	CAV	2004	DBLP DOI BibTeX RDF
22	Guillaume Lussier, Hélène Waeselynck	Deriving Test Sets from Partial Proofs.	ISSRE	2004	DBLP DOI BibTeX RDF
22	Mark Lawford, Hong Zhang 0016	Equivalence Verification of Timed Transition Models.	ACSD	2004	DBLP DOI BibTeX RDF
22	César A. Muñoz, Gilles Dowek, Victor Carreño	Modeling and verification of an air traffic concept of operations.	ISSTA	2004	DBLP DOI BibTeX RDF	air traffic management systems, model checking, theorem proving
22	Youngsik Kim, Shekhar Kopuri, Nazanin Mansouri	Automated Formal Verification of Scheduling Process Using Finite State Machines with Datapath (FSMD).	ISQED	2004	DBLP DOI BibTeX RDF
22	Engelbert Hubbers	Integrating Tools for Automatic Program Verification.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF
22	Dmitri Chkliaev, Jozef Hooman, Erik P. de Vink	Verification and Improvement of the Sliding Window Protocol.	TACAS	2003	DBLP DOI BibTeX RDF
22	Jesse Hughes, Martijn Warnier	The Coinductive Approach to Verifying Cryptographic Protocols.	WADT	2002	DBLP DOI BibTeX RDF
22	Carmen Graciani Díaz, Francisco-Jesús Martín-Mateos, Mario J. Pérez-Jiménez	Specification of Adleman's Restricted Model Using an Automated Reasoning System: Verification of Lipton's Experiment.	UMC	2002	DBLP DOI BibTeX RDF
22	Neil Henderson, Stephen Paynter	The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism.	FME	2002	DBLP DOI BibTeX RDF	retrieve relation, refinement, asynchronous communication, reification
22	Jonathan Ford, Natarajan Shankar	Formal Verification of a Combination Decision Procedure.	CADE	2002	DBLP DOI BibTeX RDF
22	Andre Renaud, Padmanabhan Krishnan	An Environment for Specifying and Verifying Security Properties.	Australian Software Engineering Conference	2001	DBLP DOI BibTeX RDF
22	Dmitri Chkliaev, Jozef Hooman, Peter van der Stok	Serializability Preserving Extensions of Concurrency Control Protocols.	Ershov Memorial Conference	1999	DBLP DOI BibTeX RDF
22	Axel Dold, Vincent Vialard	Formal Verification of a Compiler Back-End Generic Checker Program.	Ershov Memorial Conference	1999	DBLP DOI BibTeX RDF	checker-based program verification, generic specification, formal verification
22	Marcelo Glusman, Shmuel Katz	Mechanizing Proofs of Computation Equivalence.	CAV	1999	DBLP DOI BibTeX RDF
22	Hassen Saïdi, Natarajan Shankar	Abstract and Model Check While You Prove.	CAV	1999	DBLP DOI BibTeX RDF
22	Abhijit Ghosh, Ranga Vemuri	Formal Verification of Synthesized Analog Designs.	ICCD	1999	DBLP DOI BibTeX RDF
22	Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß	Case Studies in Meta-Level Theorem Proving.	TPHOLs	1998	DBLP DOI BibTeX RDF
22	S. Rajan, Natarajan Shankar, Mandayam K. Srivas	An Integration of Model Checking with Automated Proof Checking.	CAV	1995	DBLP DOI BibTeX RDF
20	Kyung-Min Kim, Jong Wook Kwak	PVS-GEN: Systematic Approach for Universal Synthetic Data Generation Involving Parameterization, Verification, and Segmentation.	Sensors	2024	DBLP DOI BibTeX RDF
20	Zhengrong Chen, Siyao Cai, A. P. Sakis Meliopoulos	A Real-time Deep Learning-based Fault Diagnosis Framework in Power Distribution System with PVs.	ISGT	2024	DBLP DOI BibTeX RDF
20	Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Andréia B. Avelar, André Luiz Galdino	Formalization of Algebraic Theorems in PVS (Invited Talk).	LPAR	2023	DBLP DOI BibTeX RDF
20	Ayu Sonoda, Paul Compagnon, Marina Reyboz, Hiroaki Nishi	Attention-PVS for Domestic Hot Water Consumption Forecasting in Individual Household.	IECON	2023	DBLP DOI BibTeX RDF
20	Aman Samson Mogos, Xiaodong Liang, C. Y. Chung 0001	Impact of Plug-in Electric Vehicle Charging and Roof-top PVs on Distribution Transformer Health: A Case Study in Saskatoon, Canada.	CCECE	2023	DBLP DOI BibTeX RDF
20	Tahir Sag	PVS: a new population-based vortex search algorithm with boosted exploration capability using polynomial mutation.	Neural Comput. Appl.	2022	DBLP DOI BibTeX RDF
20	Arian Zahedmanesh, Kashem M. Muttaqi, Danny Sutanto	An Adaptable Correlated Control for Maintaining Voltage Quality in Low-Voltage Distribution Grids Containing PVs and PEVs.	IEEE Trans. Ind. Informatics	2022	DBLP DOI BibTeX RDF
20	Muhammad Saqib Nawaz, Meng Sun 0002, Basit Shahzad, Muhammad Ikram Ullah Lali, Tariq Umer, Shaohua Wan 0001	Quality of service in IoT protocol as designs and its verification in PVS.	Trans. Emerg. Telecommun. Technol.	2022	DBLP DOI BibTeX RDF
20	John Rushby	PVS Embeddings of Propositional and Quantified Modal Logic.	CoRR	2022	DBLP DOI BibTeX RDF
20	Paolo Masci 0001	Formal analysis of the application programming interface of the PVS verification system.	J. Log. Algebraic Methods Program.	2022	DBLP DOI BibTeX RDF
20	Zaint A. Alexakis, Antonio T. Alexandridis	Optimization of MPP tracking algorithms for PVs with the impact of losses minimized.	ICCA	2022	DBLP DOI BibTeX RDF
20	Somesh Bhattacharya, Brian Azzopardi	Comparitive Analysis of Frequency Support Provided by Grid-Forming and Grid-Following PVs.	ISGT	2022	DBLP DOI BibTeX RDF
20	J. Tanner Slagel, César A. Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci 0001, Lauren White	Towards an implementation of differential dynamic logic in PVS.	SOAP@PLDI	2022	DBLP DOI BibTeX RDF
20	Paolo Masci 0001, Aaron Dutle	Proof Mate: An Interactive Proof Helper for PVS (Tool Paper).	NFM	2022	DBLP DOI BibTeX RDF
20	Nicholas Moore, Mark Lawford	A Case Study in the Automated Translation of BSV Hardware to PVS Formal Logic with Subsequent Verification.	TASE	2022	DBLP DOI BibTeX RDF
20	Di Cao, Junbo Zhao, Weihao Hu, Fei Ding 0001, Qi Huang 0001, Zhe Chen 0007, Frede Blaabjerg	Data-Driven Multi-Agent Deep Reinforcement Learning for Distribution System Decentralized Voltage Control With High Penetration of PVs.	IEEE Trans. Smart Grid	2021	DBLP DOI BibTeX RDF
20	Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, Mauricio Ayala-Rincón	Formalization of Ring Theory in PVS.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
20	M. Saqib Nawaz, Meng Sun 0002, Philippe Fournier-Viger	Proof Searching in PVS Theorem Prover Using Simulated Annealing.	ICSI (2)	2021	DBLP DOI BibTeX RDF
20	Ben L. Di Vito, Ashlie B. Hocking	Polygon Merge: A Geometric Algorithm Verified Using PVS.	NFM	2021	DBLP DOI BibTeX RDF
20	Mehrdad Bagheri-Sanjareh, Mohammad Hassan Nazari, Gevork B. Gharehpetian, Seyed Hossein Hosseinian	New approach for sizing of overloaded-capable battery for Microgrid frequency control using cooperation of PVs, BESS and smart lighting loads.	J. Intell. Fuzzy Syst.	2020	DBLP DOI BibTeX RDF
20	Hai Lu, Yuanyuan Chai, Junnan Hao, Xiaoyun Chen, Li Guo 0014, Yixin Liu	Network Simplification-Based Cluster Coordinated Optimization Method for Distributed PVs With Inadequate Measurement.	IEEE Access	2020	DBLP DOI BibTeX RDF
20	M. Saqib Nawaz, Philippe Fournier-Viger, Ji Zhang 0001	Proof Learning in PVS With Utility Pattern Mining.	IEEE Access	2020	DBLP DOI BibTeX RDF
20	Arash Baharvandi, Jamshid Aghaei, Ahmad Nikoobakht, Taher Niknam, Vahid Vahidinasab, Damian Giaouris, Phil Taylor	Linearized Hybrid Stochastic/Robust Scheduling of Active Distribution Networks Encompassing PVs.	IEEE Trans. Smart Grid	2020	DBLP DOI BibTeX RDF
20	Sachidananda Sen, Vishal Kumar	Simplified Modeling and HIL Validation of Solar PVs and Storage-Based Islanded Microgrid With Generation Uncertainties.	IEEE Syst. J.	2020	DBLP DOI BibTeX RDF
20	Asmaa Zaz, Mohammed Bakkali, Mohammed Ouassaid, Yasunobu Ashie, Mounir Ghogho	Modelling Effects of Rooftop PVs on Outdoor Temperatures: The Case of Low Latitude Neighbourhoods.	Intelligent Environments (Workshops)	2020	DBLP DOI BibTeX RDF
20	Xiaoxin An, Amer Tahat, Binoy Ravindran	A Validation Methodology for OCaml-to-PVS Translation.	NFM	2020	DBLP DOI BibTeX RDF
20	Aya Shimura, Mamoru Sawahashi, Satoshi Nagata, Yoshihisa Kishiyama	Physical Cell ID Detection Probabilities Using Frequency Domain PVS Transmit Diversity for NB-IoT Radio Interface.	IEICE Trans. Commun.	2019	DBLP DOI BibTeX RDF
20	Poria Astero, Lennart Söder	Improving Hosting Capacity of Rooftop PVs by Quadratic Control of an LV-Central BSS.	IEEE Trans. Smart Grid	2019	DBLP DOI BibTeX RDF
20	M. Saqib Nawaz, Meng Sun 0002	Using PVS for Modeling and Verification of Probabilistic Connectors.	FSEN	2019	DBLP DOI BibTeX RDF
20	M. Saqib Nawaz, Meng Sun 0002, Philippe Fournier-Viger	Proof Guidance in PVS with Sequential Pattern Mining.	FSEN	2019	DBLP DOI BibTeX RDF
20	Gustavo A. Ramos, David Celeita, Tatiana Quintero	Reverse Power Flow Analyzer (RPFA): A tool to assess the impact of PVs in distribution systems.	IAS	2019	DBLP DOI BibTeX RDF
20	David E. Narváez	Formalizing CNF SAT Symmetry Breaking in PVS.	NFM	2019	DBLP DOI BibTeX RDF
20	Thodoris Kottas, Athanasios D. Karlis, Yiannis S. Boutalis	A Novel Control Algorithm for DC Motors Supplied by PVs Using Fuzzy Cognitive Networks.	IEEE Access	2018	DBLP DOI BibTeX RDF
20	Hyun-Gu Lee, Gyu-Gwang Kim, Byeong Gwan Bhang, David Kwangsoon Kim, Neungsoo Park, Hyung Keun Ahn	Design Algorithm for Optimum Capacity of ESS Connected With PVs Under the RPS Program.	IEEE Access	2018	DBLP DOI BibTeX RDF
20	Cinzia Bernardeschi, Andrea Domenici, Paolo Masci 0001	A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems.	IEEE Trans. Software Eng.	2018	DBLP DOI BibTeX RDF
20	Anthony Savidis	There is more to PCG than Meets the Eye: NPC AI, Dynamic Camera, PVS and Lightmaps.	CoRR	2018	DBLP BibTeX RDF
20	Josh Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford	Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application.	J. Autom. Reason.	2018	DBLP DOI BibTeX RDF
20	Ling Shi, Yongxin Zhao, Yang Liu 0003, Jun Sun 0001, Jin Song Dong, Shengchao Qin	A UTP semantics for communicating processes with shared variables and its formal encoding in PVS.	Formal Aspects Comput.	2018	DBLP DOI BibTeX RDF
20	M. Saqib Nawaz, Meng Sun 0002	A Formal Design Model for Genetic Algorithms Operators and its Encoding in PVS.	BDIOT	2018	DBLP DOI BibTeX RDF
20	Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino	Formalizing Ring Theory in PVS.	ITP	2018	DBLP DOI BibTeX RDF
20	Maryam Alami Chentoufi, Rachid Ellaia	Adaptive traffic signal optimization considering emergency vehicle preemption and tram priority using PVS algorithm.	SCA	2018	DBLP DOI BibTeX RDF
20	Frédéric Gilbert 0002	Extending higher-order logic with predicate subtyping: Application to PVS. (Extension de la logique d'ordre supérieur avec le sous-typage par prédicats).		2018	RDF
20	Felicidad Aguado, Pablo Ascariz, Pedro Cabalar, Gilberto Pérez 0001, Concepción Vidal	Verification for ASP denotational semantics: A case study using the PVS theorem prover.	Log. J. IGPL	2017	DBLP DOI BibTeX RDF
20	Shunsuke Kawano, Kohei Murakami, Shinya Yoshizawa, Yasuhiro Hayashi	Basic study on application of real-time satellite-observed solar radiation data for centralized voltage control in distribution networks with PVs.	ISGT	2017	DBLP DOI BibTeX RDF
20	Natarajan Shankar	Formalizing Hoare Logic in PVS.	SETSS	2017	DBLP DOI BibTeX RDF
20	Frédéric Gilbert 0002	Proof Certificates in PVS.	ITP	2017	DBLP DOI BibTeX RDF
20	Michael Kohlhase, Dennis Müller 0001, Sam Owre, Florian Rabe 0001	Making PVS Accessible to Generic Services by Interpretation in a Universal Format.	ITP	2017	DBLP DOI BibTeX RDF
20	Ashlie B. Hocking, M. Anthony Aiello	The Measurement Library: Representing Physical Types in PVS.	AFM@NFM	2017	DBLP DOI BibTeX RDF
20	Aya Shimura, Mamoru Sawahashi, Satoshi Nagata, Yoshihisa Kishiyama	Performance of physical cell ID detection using PVS based transmit diversity for NB-IoT.	WPMC	2017	DBLP DOI BibTeX RDF
20	Yasunori Isozaki, Shinya Yoshizawa, Yu Fujimoto, Hideaki Ishii, Isao Ono, Takashi Onoda, Yasuhiro Hayashi	Detection of Cyber Attacks Against Voltage Control in Distribution Power Grids With PVs.	IEEE Trans. Smart Grid	2016	DBLP DOI BibTeX RDF
20	Kalyani Singh, Brent Auernheimer	Formal Specification of Multi-Window User Interface in PVS.	HCI (26)	2016	DBLP DOI BibTeX RDF
20	Josh Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford	Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application.	NFM	2016	DBLP DOI BibTeX RDF
20	Mauricio Ayala-Rincón, Maribel Fernández, Ana Cristina Rocha Oliveira	Completeness in PVS of a Nominal Unification Algorithm.	LSFA	2015	DBLP DOI BibTeX RDF
20	Mauricio Ayala-Rincón	Formalising Confluence in PVS.	DCM	2015	DBLP DOI BibTeX RDF
20	Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, Josh Newell, Vera Chow, David Tremaine	Formal Verification of Real-Time Function Blocks Using PVS.	ESSS	2015	DBLP DOI BibTeX RDF
20	Paolo Masci 0001, Paul Curzon, Dominic Furniss, Ann Blandford	Using PVS to support the analysis of distributed cognition systems.	Innov. Syst. Softw. Eng.	2015	DBLP DOI BibTeX RDF
20	Paolo Masci 0001, Patrick Oladimeji, Yi Zhang 0051, Paul L. Jones, Paul Curzon, Harold W. Thimbleby	PVSio-web 2.0: Joining PVS to HCI.	CAV (1)	2015	DBLP DOI BibTeX RDF
20	Sarjiya, Yusuf Susilo Wijoyo, Rayyan	Electricity tariff of Bunaken hybrid Genset-PVs-battery system based on LRMC method.	ICCSCE	2015	DBLP DOI BibTeX RDF
20	Sjaak Smetsers, Ken Madlener, Marko C. J. D. van Eekelen	Formalizing Bialgebraic Semantics in PVS 6.0.	WPTE@RDP	2015	DBLP DOI BibTeX RDF