Skip to content

Commit a0bed70

Browse files
ttjttj
committed
Update readmes for NNV 3 and other minor updates
1 parent 77d2c1f commit a0bed70

File tree

7 files changed

+176
-25
lines changed

7 files changed

+176
-25
lines changed

‎README.md‎

Lines changed: 43 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,49 @@ _Previous_
7676
7777
Open MATLAB, then go to the `/code/nnv/` folder and execute the `uninstall.m` script.
7878
79-
# Getting started with NNV
79+
---
80+
81+
# What's New in NNV 3.0
82+
83+
NNV 3.0 introduces major new verification capabilities:
84+
85+
- **VolumeStar**: Verification of video and 3D volumetric data (medical images)
86+
- **FairNNV**: Formal verification of neural network fairness
87+
- **Probabilistic Verification**: Scalable conformal prediction-based analysis
88+
- **Weight Perturbation Analysis**: Verification under quantization/hardware errors
89+
- **Time-Dependent Networks**: Variable-length time series verification
90+
- **Malware Detection**: New cybersecurity verification domain
91+
92+
See [README_NNV3_CONTRIBUTIONS.md](README_NNV3_CONTRIBUTIONS.md) for full details on NNV 3.0 features.
93+
94+
## Documentation
95+
96+
| Document | Description |
97+
|----------|-------------|
98+
| [README_NNV3_CONTRIBUTIONS.md](README_NNV3_CONTRIBUTIONS.md) | NNV 3.0 new features and contributions |
99+
| [README_TEST.md](README_TEST.md) | Testing documentation and coverage |
100+
| [code/nnv/examples/README.md](code/nnv/examples/README.md) | Examples navigation guide |
101+
| [code/nnv/examples/QuickStart/](code/nnv/examples/QuickStart/) | Getting started examples |
102+
| [code/nnv/examples/Tutorial/](code/nnv/examples/Tutorial/) | Step-by-step tutorials |
103+
104+
---
105+
106+
# Getting started with NNV
107+
108+
### Quick Start
109+
110+
**New to NNV?** Start with the [QuickStart examples](code/nnv/examples/QuickStart/) for installation verification and your first neural network verification.
111+
112+
```matlab
113+
cd examples/QuickStart
114+
test_installation % Verify your setup
115+
simple_verification % Your first verification
116+
```
117+
118+
**Troubleshooting?** Run the diagnostic tool:
119+
```matlab
120+
check_nnv_setup()
121+
```
80122

81123
### [Tutorial](code/nnv/examples/Tutorial)
82124

‎README_TEST.md‎

Lines changed: 28 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# NNV Test Suite Documentation
22

3-
*Last Updated: November 29, 2025*
3+
*Last Updated: December 1, 2025*
44

55
---
66

@@ -15,7 +15,7 @@ addpath(fullfile(pwd, 'tests', 'test_utils'));
1515
[test_results, regression_results] = run_tests_with_regression('tests', 'compare', true, 'verbose', true);
1616
```
1717

18-
This single command runs **743 tests** including:
18+
This single command runs **833 tests** (full suite) or **470 tests** (quick mode) including:
1919
- All soundness tests (layers, sets, solvers)
2020
- All regression tests (NNCS, NN, verification)
2121
- All figure-saving tests (99 figures)
@@ -27,13 +27,38 @@ This single command runs **743 tests** including:
2727

2828
| Metric | Count | Status |
2929
|--------|-------|--------|
30-
| Total Tests | 743 | All Passing |
30+
| Full Suite Tests | 833 | All Passing |
31+
| Quick Mode Tests | 470 | All Passing |
3132
| Figures Saved | 99 | 100% Coverage |
3233
| Baselines | 46 | All Matched |
3334
| Regressions | 0 | None Detected |
3435

3536
---
3637

38+
## Code Coverage
39+
40+
NNV 3.0 includes code coverage tracking via the `track_coverage.m` utility.
41+
42+
| Directory | Coverage |
43+
|-----------|----------|
44+
| Overall | **48.6%** |
45+
| engine/nn/ | 86.2% |
46+
| engine/set/ | 88.9% |
47+
| engine/utils/ | 23.1% |
48+
| engine/nncs/ | 18.2% |
49+
| engine/hyst/ | 0.0% |
50+
51+
See [TEST_COVERAGE.md](TEST_COVERAGE.md) for the full coverage report.
52+
53+
### Running Coverage Analysis
54+
55+
```matlab
56+
addpath(fullfile(pwd, 'tests', 'test_utils'));
57+
coverage = track_coverage('tests', 'quick_mode', true);
58+
```
59+
60+
---
61+
3762
## Test Infrastructure Overview
3863

3964
| Directory | Purpose | Approx Count |

‎code/nnv/engine/adjust_glpk.m‎

Lines changed: 60 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,61 @@
1-
fid = fopen('../tbxmanager/toolboxes/glpkmex/1.0/glnxa64/glpkmex_1_0_glnxa64/glpk.m');
2-
cac = textscan( fid, '%s', 'Delimiter','\n','whitespace', '');
3-
fclose(fid)
4-
fid = fopen('../tbxmanager/toolboxes/glpkmex/1.0/glnxa64/glpkmex_1_0_glnxa64/glpk.m', 'w');
5-
change_here = 372;
6-
for jj = 1 : change_here-1
7-
fprintf(fid, '%s\n', cac{1}{jj});
1+
function adjust_glpk()
2+
% ADJUST_GLPK - Fix glpkmex for compatibility with NNV
3+
%
4+
% This function modifies the glpk.m file to comment out a problematic
5+
% 'clear glpkcc' statement that can cause issues during reachability
6+
% analysis.
7+
%
8+
% Platform-aware: Works on Windows (win64), Linux (glnxa64), and
9+
% macOS (maci64/maca64).
10+
%
11+
% Usage:
12+
% adjust_glpk()
13+
%
14+
% Note: This is typically called automatically by install.m
15+
16+
try
17+
% Determine platform
18+
arch = computer('arch'); % 'glnxa64', 'win64', 'maci64', or 'maca64'
19+
20+
% Construct platform-specific path
21+
glpk_base = fullfile('..', 'tbxmanager', 'toolboxes', 'glpkmex', '1.0', arch);
22+
glpk_folder = sprintf('glpkmex_1_0_%s', arch);
23+
filename = fullfile(glpk_base, glpk_folder, 'glpk.m');
24+
25+
% Check if file exists
26+
if ~isfile(filename)
27+
fprintf('Note: glpkmex not found for platform %s\n', arch);
28+
return;
29+
end
30+
31+
% Read the file
32+
fid = fopen(filename);
33+
if fid == -1
34+
fprintf('Warning: Could not open %s\n', filename);
35+
return;
36+
end
37+
cac = textscan(fid, '%s', 'Delimiter', '\n', 'whitespace', '');
38+
fclose(fid);
39+
40+
% Write modified file
41+
fid = fopen(filename, 'w');
42+
if fid == -1
43+
fprintf('Warning: Could not write to %s\n', filename);
44+
return;
45+
end
46+
47+
change_here = 372; % Line with 'clear glpkcc;'
48+
for jj = 1 : min(change_here-1, length(cac{1}))
49+
fprintf(fid, '%s\n', cac{1}{jj});
50+
end
51+
fprintf(fid, '%s\n', '%clear glpkcc;'); % Comment out the clear statement
52+
for jj = change_here+1 : length(cac{1})
53+
fprintf(fid, '%s\n', cac{1}{jj});
54+
end
55+
fclose(fid);
56+
57+
fprintf('Successfully adjusted glpk.m for platform %s\n', arch);
58+
catch ME
59+
fprintf('Warning: Could not adjust glpk.m: %s\n', ME.message);
860
end
9-
fprintf(fid, '%s\n', '%clear glpkcc;');
10-
for jj = change_here+1: length(cac{1})
11-
fprintf(fid, '%s\n', cac{1}{jj});
12-
end
13-
fclose(fid);
61+
end

‎code/nnv/examples/QuickStart/README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
# NNV Quick Start Guide
22

3+
*Part of NNV 3.0 - see [README_NNV3_CONTRIBUTIONS.md](../../../../README_NNV3_CONTRIBUTIONS.md) for new features*
4+
35
Welcome to NNV! This folder contains simple examples to get you started quickly.
46

57
## Prerequisites

‎code/nnv/examples/README.md‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
# NNV Examples
22

3+
*Part of NNV 3.0 - see [README_NNV3_CONTRIBUTIONS.md](../../../README_NNV3_CONTRIBUTIONS.md) for new features*
4+
35
This directory contains examples demonstrating NNV's neural network verification capabilities.
46

57
## Getting Started
68

7-
**New to NNV?** Start with the `Tutorial/` folder for step-by-step examples with explanations.
9+
**New to NNV?** Start with the [QuickStart/](QuickStart/) folder for installation verification, then explore `Tutorial/` for step-by-step examples with explanations.
810

911
## Directory Guide
1012

‎code/nnv/examples/Tutorial/readme.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
# NNV Tutorial Examples
2+
3+
*Part of NNV 3.0 - see [README_NNV3_CONTRIBUTIONS.md](../../../../README_NNV3_CONTRIBUTIONS.md) for new features*
4+
5+
## New to NNV?
6+
7+
Start with the [QuickStart examples](../QuickStart/) for basic installation verification and your first neural network verification.
8+
9+
---
10+
111
# Neural Network Verification for Medical Imaging Analysis - NNV Tutorial at SPIE 2025
212

313
Previous tutorials at

‎code/nnv/install.m‎

Lines changed: 30 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -86,23 +86,45 @@
8686
ver()
8787

8888
function adjust_glpk()
89+
% Platform-specific path handling for glpkmex
8990
try
90-
filename = 'tbxmanager/toolboxes/glpkmex/1.0/glnxa64/glpkmex_1_0_glnxa64/glpk.m';
91+
arch = computer('arch'); % 'glnxa64', 'win64', 'maci64', or 'maca64'
92+
93+
% Construct platform-specific path
94+
glpk_base = fullfile('tbxmanager', 'toolboxes', 'glpkmex', '1.0', arch);
95+
glpk_folder = sprintf('glpkmex_1_0_%s', arch);
96+
filename = fullfile(glpk_base, glpk_folder, 'glpk.m');
97+
98+
% Check if file exists for this platform
99+
if ~isfile(filename)
100+
fprintf('Note: glpkmex not found for platform %s (may not be needed)\n', arch);
101+
return;
102+
end
103+
91104
fid = fopen(filename);
92-
cac = textscan( fid, '%s', 'Delimiter','\n','whitespace', '');
105+
if fid == -1
106+
return; % Could not open file
107+
end
108+
cac = textscan(fid, '%s', 'Delimiter', '\n', 'whitespace', '');
93109
fclose(fid);
94-
filename2 = 'tbxmanager/toolboxes/glpkmex/1.0/glnxa64/glpkmex_1_0_glnxa64/glpk2.m';
110+
111+
filename2 = fullfile(glpk_base, glpk_folder, 'glpk2.m');
95112
fid = fopen(filename2, 'w');
113+
if fid == -1
114+
return; % Could not create temp file
115+
end
116+
96117
change_here = 372;
97-
for jj = 1 : change_here-1
98-
fprintf(fid, '%s\n', cac{1}{jj});
118+
for jj = 1 : min(change_here-1, length(cac{1}))
119+
fprintf(fid, '%s\n', cac{1}{jj});
99120
end
100121
fprintf(fid, '%s\n', '%clear glpkcc;');
101-
for jj = change_here+1: length(cac{1})
102-
fprintf(fid, '%s\n', cac{1}{jj});
122+
for jj = change_here+1 : length(cac{1})
123+
fprintf(fid, '%s\n', cac{1}{jj});
103124
end
104125
fclose(fid);
105-
movefile(filename2,filename,'f')
126+
movefile(filename2, filename, 'f');
106127
catch
128+
% Silently ignore errors - glpk adjustment is optional
107129
end
108130
end

0 commit comments

Comments
 (0)