Groups keyboard shortcuts have been updated

Dismiss

See shortcuts

PVS verification system

Contact owners and managers

1–30 of 55

0 selected

Mariano Moscato

May 29

PVS Day at NFM 2025, June 10, 2025

------------------------------------------------------- Call for Participation: PVS DAY @ NFM 2025 --

unread,

PVS Day at NFM 2025, June 10, 2025

------------------------------------------------------- Call for Participation: PVS DAY @ NFM 2025 --

May 29

Feb 5

Hello everyone, I have a question on the Typecheck phase of a pvs theory. I have two pvs theories

unread,

Hello everyone, I have a question on the Typecheck phase of a pvs theory. I have two pvs theories

Feb 5

THAYNARA ARIELLY DE LIMA

Jan 27

CICM 2025 - Call for Workshops

Dear colleagues, I hope this message finds you well. This year, the 18th Conference on Intelligent

unread,

CICM 2025 - Call for Workshops

Dear colleagues, I hope this message finds you well. This year, the 18th Conference on Intelligent

Jan 27

12/5/24

Rewriting/expanding definitions (performance)

Hi everyone, I'm developing a pvs strategy and I have noticed that the bottleneck of it is when I

unread,

Rewriting/expanding definitions (performance)

Hi everyone, I'm developing a pvs strategy and I have noticed that the bottleneck of it is when I

12/5/24

10/17/24

Expressing provability in PVS

Hi everyone, I was wondering: Is there in PVS a way to express, within a theorem or lemma declaration

unread,

Expressing provability in PVS

Hi everyone, I was wondering: Is there in PVS a way to express, within a theorem or lemma declaration

10/17/24

Giulia Sindoni, Sam Owre2

9/26/24

Heap exhaustion

Hi Giulia, This is (partially) discussed in Section 3.2.3 of the SBCL document (https://www.sbcl.org/

unread,

Heap exhaustion

Hi Giulia, This is (partially) discussed in Section 3.2.3 of the SBCL document (https://www.sbcl.org/

9/26/24

Giulia Sindoni, Mariano Moscato5

9/25/24

TCCs going from "proved-complete" to "unfinished"

Thank you Mariano, that is really helpful! Giulia On Friday, September 20, 2024 at 5:23:13 AM UTC+2

unread,

TCCs going from "proved-complete" to "unfinished"

Thank you Mariano, that is really helpful! Giulia On Friday, September 20, 2024 at 5:23:13 AM UTC+2

9/25/24

Peter Gumm, Mariano Moscato3

9/17/24

Very simple question regarding typepred or the like

Thanks for your explanation. It makes perfect sense. H.Peter On Monday, September 16, 2024 at 5:16:52

unread,

Very simple question regarding typepred or the like

Thanks for your explanation. It makes perfect sense. H.Peter On Monday, September 16, 2024 at 5:16:52

9/17/24

Maxwell Brainerd, Mariano Moscato2

6/12/24

Compatibility with Silicon Chips

Hi Maxwell, We are actively working on VSCode-PVS to add support for the new version of PVS (8.0)

unread,

Compatibility with Silicon Chips

Hi Maxwell, We are actively working on VSCode-PVS to add support for the new version of PVS (8.0)

6/12/24

4/24/24

vscode-pvs 1.0.65 released!

A new version of vscode-pvs (v1.0.65) is now available in the marketplace (https://marketplace.

unread,

vscode-pvs 1.0.65 released!

A new version of vscode-pvs (v1.0.65) is now available in the marketplace (https://marketplace.

4/24/24

Mariano Moscato

3/27/24

LSFA 2024: First Call for Papers

LSFA 2024: CALL FOR PAPERS The 19th International Workshop on Logical and Semantic Frameworks with

unread,

LSFA 2024: First Call for Papers

LSFA 2024: CALL FOR PAPERS The 19th International Workshop on Logical and Semantic Frameworks with

3/27/24

Peter Gumm, Paolo Masci2

2/12/24

vscode-pvs freezes my lubuntu box

Peter, thank you for reporting this problem. We will look into this ASAP and post a solution in this

unread,

vscode-pvs freezes my lubuntu box

Peter, thank you for reporting this problem. We will look into this ASAP and post a solution in this

2/12/24

2/12/24

Here is the screenshot

unread,

Here is the screenshot

2/12/24

Max H, Paolo Masci2

6/2/23

PVS successfully typechecks everything

Hi, thank you for reaching out. It is likely that something went wrong during the installation of PVS

unread,

PVS successfully typechecks everything

Hi, thank you for reaching out. It is likely that something went wrong during the installation of PVS

6/2/23

Victor Candeira, Paolo Masci4

4/14/23

Begginner - Open PVSio following the tutorial

Hi, the bug with the vscode-pvs menu should be resolved in this new pre-release 1.0.64-theta: https:/

unread,

Begginner - Open PVSio following the tutorial

Hi, the bug with the vscode-pvs menu should be resolved in this new pre-release 1.0.64-theta: https:/

4/14/23

4/14/23

vscode-pvs-1.0.64 pre-release

Hi Everyone, at the following link you can find a new pre-release 1.0.64-theta of vscode-pvs: https:/

unread,

vscode-pvs-1.0.64 pre-release

Hi Everyone, at the following link you can find a new pre-release 1.0.64-theta of vscode-pvs: https:/

4/14/23

3/31/23

Building PVS on ARM-based Macs

It would be great if others could test out my build instructions so we catch problems before this can

unread,

Building PVS on ARM-based Macs

It would be great if others could test out my build instructions so we catch problems before this can

3/31/23

Kai Engelhardt, Mariano Moscato3

3/27/23

Looking for a non-simplifying extensionality rule

Thanks for the hint! Hopefully I'll remember that next time. I ended up proving some semi-useful

unread,

Looking for a non-simplifying extensionality rule

Thanks for the hint! Hopefully I'll remember that next time. I ended up proving some semi-useful

3/27/23

Alberto Ercolani, Paolo Masci5

10/20/22

Feature request: proving TCCs for specific lemma only

Hey Paolo, I tried the pre-release and found the new feature to be even better than expected! The

unread,

Feature request: proving TCCs for specific lemma only

Hey Paolo, I tried the pre-release and found the new feature to be even better than expected! The

10/20/22

Paolo Masci, Tanner Slagel5

8/12/22

vscode-pvs-1.0.63 pre-release

Really like the improved NASALib search here Paolo! On Wednesday, July 20, 2022 at 1:56:12 PM UTC-4

unread,

vscode-pvs-1.0.63 pre-release

Really like the improved NASALib search here Paolo! On Wednesday, July 20, 2022 at 1:56:12 PM UTC-4

8/12/22

Julin S, Paolo Masci2

6/28/22

Trivial proof without grind

Yes, after removing the universal quantifier (skeep) and expanding the relevant definitions, you can

unread,

Trivial proof without grind

Yes, after removing the universal quantifier (skeep) and expanding the relevant definitions, you can

6/28/22

Tanner Slagel, … Paolo Masci4

6/25/22

Emulating PVS on M1 macs

They are both slow because of the emulation with Qemu. The difference in the performance is probably

unread,

Emulating PVS on M1 macs

They are both slow because of the emulation with Qemu. The difference in the performance is probably

6/25/22

Julin S, Paolo Masci6

6/23/22

Julin, yes, the SBCL version of PVS will be supported in future releases. The problem you encountered

unread,

Julin, yes, the SBCL version of PVS will be supported in future releases. The problem you encountered

6/23/22

Alberto Ercolani, Tanner Slagel11

6/22/22

Exactly generic N elements in HOL

Alberto, I am glad to hear the formalization worked out! Feel free to reach out with any future work

unread,

Exactly generic N elements in HOL

Alberto, I am glad to hear the formalization worked out! Feel free to reach out with any future work

6/22/22

5/23/22

vscode-pvs-1.0.62 + video tutorial on vscode-pvs + NFM

Everyone, here's the latest news on vscode-pvs: 1. A new version vscode-pvs-1.0.62 is now

unread,

vscode-pvs-1.0.62 + video tutorial on vscode-pvs + NFM

Everyone, here's the latest news on vscode-pvs: 1. A new version vscode-pvs-1.0.62 is now

5/23/22

5/3/22

vscode-pvs-1.0.61 pre-release

Another pre-release vscode-pvs-1.0.61-delta is available at the following link: https://nationalia-my

unread,

vscode-pvs-1.0.61 pre-release

Another pre-release vscode-pvs-1.0.61-delta is available at the following link: https://nationalia-my

5/3/22

3/17/22

vscode-pvs-1.0.60

FYI, I have pushed a new version vscode-pvs-1.0.60 to the Visual Studio Code marketplace that fixes

unread,

vscode-pvs-1.0.60

FYI, I have pushed a new version vscode-pvs-1.0.60 to the Visual Studio Code marketplace that fixes

3/17/22

2/2/22

vscode-pvs-1.0.59 pre-release

At the following link you can find an updated pre-release version vscode-pvs-1.0.59-epsilon: https://

unread,

vscode-pvs-1.0.59 pre-release

At the following link you can find an updated pre-release version vscode-pvs-1.0.59-epsilon: https://

2/2/22

12/16/21

vscode-pvs-1.0.58 pre-release

Hi Everyone, I'm sharing a new pre-release vscode-pvs-1.0.58-theta with few additional fixes

unread,

vscode-pvs-1.0.58 pre-release

Hi Everyone, I'm sharing a new pre-release vscode-pvs-1.0.58-theta with few additional fixes

12/16/21

Alberto Ercolani2

9/22/21

Proving predicate-subtype equivalence

Extensionality rules did provide me a way to deduce equality. Commands in pages 65 to 68 of the

unread,

Proving predicate-subtype equivalence

Extensionality rules did provide me a way to deduce equality. Commands in pages 65 to 68 of the

9/22/21

Search

Clear search

Close search

Google apps

Main menu