## Features.Home History

Hide minor edits - Show changes to output - Cancel

Changed line 12 from:

** New set of types, namely 'Integer' and 'Reals'

to:

** New set of types, namely 'Integer' and 'Reals', and Uninterpreted Functions

Changed line 14 from:

*** AIGER, VMT, BTOR (~~via~~ external script)

to:

*** AIGER, VMT, BTOR (this last via an external script)

Changed lines 1-2 from:

(:title ~~Documentation~~ :)

to:

(:title Features :)

Changed line 5 from:

For a detailed description of the ~~functionalities~~ provided by nuXmv, we suggest to read

to:

For a detailed description of the features provided by nuXmv, we suggest to read

Changed lines 5-8 from:

to:

For a detailed description of the functionalities provided by nuXmv, we suggest to read

the [[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|User Manual (pdf)]].

Below we list the most important ones.

the [[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|User Manual (pdf)]].

Below we list the most important ones.

Changed lines 1-2 from:

(:title ~~Features~~ :)

to:

(:title Documentation :)

Changed lines 4-5 from:

to:

Changed lines 8-13 from:

** ~~support~~ for the [[http://fmv.jku.at/aiger/|AIGER]] format

**~~new~~ set of types, namely 'Integer' and 'Reals'

* New ~~model checking algorithms for finite state systems~~

** ~~Full support for PSL model checking~~

**

to:

** Support for the [[http://fmv.jku.at/aiger/|AIGER]] format

** New set of types, namely 'Integer' and 'Reals'

** New dumps of model in several external formats

*** AIGER, VMT, BTOR (via external script)

* New model checking algorithms for finite-state systems

** New set of types, namely 'Integer' and 'Reals'

** New dumps of model in several external formats

*** AIGER, VMT, BTOR (via external script)

* New model checking algorithms for finite-state systems

Changed lines 17-18 from:

** ~~IC3~~

to:

** IC3 based algorithms

** K-liveness

** K-liveness

Changed lines 20-22 from:

*** Reachability analysis ~~guided by a regular~~ expression

* New model checking algorithms for infinite~~ ~~state systems

* New model checking algorithms for infinite

to:

*** Reachability analysis and invariant checking guided by a regular expression

* New model checking algorithms for infinite-state systems

* New model checking algorithms for infinite-state systems

Added line 26:

*** K-liveness

Changed line 28 from:

*** ~~IC3~~

to:

*** IC3 based algorithms

Changed line 31 from:

*** Refinement via Unsatisfiable Core and Interpolation

to:

**** Refinement via Unsatisfiable Core and Interpolation

Added line 33:

**** Refinement via Unsatisfiable Core and Interpolation

Deleted lines 42-46:

*** Property satisfiability

*** Property entailment

*** Unsatisfiable core extraction

*** Property realizability

Added lines 35-37:

** Explicit FSM view generation

*** Dump in .xmi format

*** Subject to predicate abstraction

*** Dump in .xmi format

*** Subject to predicate abstraction

Changed lines 12-15 from:

** Range Recoding

** Free input propagation

to:

Added lines 35-37:

** Model simplification and recoding techniques

*** Range Recoding

*** Free input propagation

*** Range Recoding

*** Free input propagation

Deleted lines 35-39:

(:comment Some less important details

** Abstraction via AllSMT, and in combiation with BDDs

*** Refinement via Unsatisfiable Core and Interpolation

)

Added line 9:

** support for the [[http://fmv.jku.at/aiger/|AIGER]] format

Changed lines 11-13 from:

*~~* support for the [[http://fmv.jku.at/aiger/|AIGER]] format~~

* ~~new advanced model checking algorithms for synchronous~~ systems

to:

* Model simplification and recoding techniques

** Range Recoding

** Free input propagation

* New model checking algorithms for finite state systems

Changed line 19 from:

*** ~~[[http://www.kenmcmil.com/pubs/CAV03.pdf|~~CAV ~~2003]] ~~Mc Millan algorithm

to:

*** CAV'03 Mc Millan's interpolation algorithm

Added line 21:

** IC3

Changed lines 24-26 from:

*~~* Counter-Example Guided Abstraction Refinement (CEGAR)~~

*** Basic abstraction vial AllSMT

**~~* Advanced abstraction based on BDD and SMT~~

*** Basic abstraction vial AllSMT

to:

* New model checking algorithms for infinite state systems

** SMT-based techniques

*** Bounded Model Checking

*** K-induction

*** Interpolation Based

*** IC3

** Abstraction based techniques

*** Counter-Example Guided Abstraction Refinement (CEGAR)

Changed lines 34-40 from:

** ~~Infinite state model checking based on SMT techniques~~

*** Bounded Model Checking via SMT

**~~*~~ Abstraction ~~based~~

** Compositional reasoning techniques

** Model simplification and recoding techniques

*** ~~Range Recoding~~

*** Free input propagation

*** Bounded Model Checking via SMT

** Compositional reasoning techniques

** Model simplification and recoding techniques

*** Free input propagation

to:

*** K-induction with implicit abstraction

*** IC3 with implicit abstraction

(:comment Some less important details

** Abstraction via AllSMT, and in combiation with BDDs

*** Refinement via Unsatisfiable Core and Interpolation

)

*** IC3 with implicit abstraction

(:comment Some less important details

** Abstraction via AllSMT, and in combiation with BDDs

*** Refinement via Unsatisfiable Core and Interpolation

)

Changed line 47 from:

*** Property realizability

to:

*** Property realizability

Changed line 8 from:

* An extended ~~language~~

to:

* An extended language for synchronous systems

Deleted line 9:

Changed lines 11-12 from:

* new advanced model checking ~~algorithms~~

to:

* new advanced model checking algorithms for synchronous systems

Changed lines 31-32 from:

** Requirements ~~Analysis~~

*** Hybrid and Discrete

*** Hybrid and Discrete

to:

** Discrete Requirements Analysis

Changed lines 35-41 from:

*** Property ~~realizability~~

** Dependability Assessment

*** Fault tree analysis

*** FMEA analysis

*** FDIR verification

*** Diagnosability checks

** Dependability Assessment

*** Fault tree analysis

*** FMEA analysis

*** FDIR verification

*** Diagnosability checks

to:

*** Property realizability

Changed line 9 from:

** new constructs to represent network of (hybrid-)automata (~~HyDy~~)

to:

** new constructs to represent network of (hybrid-)automata (HyDi)

Changed line 9 from:

** new constructs to represent network of (hybrid-)~~automata~~

to:

** new constructs to represent network of (hybrid-)automata (HyDy)

Changed line 29 from:

* An extended set of ~~features~~

to:

* An extended set of functionalities

Added lines 3-4:

(:comment Here the idea is to create several pages one per each category :)

Changed lines 8-10 from:

** new set of types, namely 'Integer' and 'Reals'~~;~~

** new constructs to represent network of (hybrid-)automata~~;~~

** support for the [[http://fmv.jku.at/aiger/|AIGER]] ~~format;~~

to:

** new set of types, namely 'Integer' and 'Reals'

** new constructs to represent network of (hybrid-)automata

** support for the [[http://fmv.jku.at/aiger/|AIGER]] format

** new constructs to represent network of (hybrid-)automata

** support for the [[http://fmv.jku.at/aiger/|AIGER]] format

Added line 12:

** Full support for PSL model checking

Added lines 19-21:

*** Basic abstraction vial AllSMT

*** Advanced abstraction based on BDD and SMT

*** Refinement via Unsatisfiable Core and Interpolation

*** Advanced abstraction based on BDD and SMT

*** Refinement via Unsatisfiable Core and Interpolation

Added lines 23-24:

*** Bounded Model Checking via SMT

*** Abstraction based

*** Abstraction based

Added lines 27-28:

*** Range Recoding

*** Free input propagation

*** Free input propagation

Added line 31:

*** Hybrid and Discrete

Changed line 8 from:

** support for the [[http://aiger|AIGER]] format;

to:

** support for the [[http://fmv.jku.at/aiger/|AIGER]] format;

Added lines 1-30:

(:title Features :)

The following is an incomplete list of the provided features:

* An extended language

** new set of types, namely 'Integer' and 'Reals';

** new constructs to represent network of (hybrid-)automata;

** support for the [[http://aiger|AIGER]] format;

* new advanced model checking algorithms

** Interpolation based invariant checking

*** [[http://www.kenmcmil.com/pubs/CAV03.pdf|CAV 2003]] Mc Millan algorithm

*** Interpolation sequences algorithm

** Guided reachability

*** Reachability analysis guided by a regular expression

** Counter-Example Guided Abstraction Refinement (CEGAR)

** Infinite state model checking based on SMT techniques

** Compositional reasoning techniques

** Model simplification and recoding techniques

* An extended set of features

** Requirements Analysis

*** Property satisfiability

*** Property entailment

*** Unsatisfiable core extraction

*** Property realizability

** Dependability Assessment

*** Fault tree analysis

*** FMEA analysis

*** FDIR verification

*** Diagnosability checks

The following is an incomplete list of the provided features:

* An extended language

** new set of types, namely 'Integer' and 'Reals';

** new constructs to represent network of (hybrid-)automata;

** support for the [[http://aiger|AIGER]] format;

* new advanced model checking algorithms

** Interpolation based invariant checking

*** [[http://www.kenmcmil.com/pubs/CAV03.pdf|CAV 2003]] Mc Millan algorithm

*** Interpolation sequences algorithm

** Guided reachability

*** Reachability analysis guided by a regular expression

** Counter-Example Guided Abstraction Refinement (CEGAR)

** Infinite state model checking based on SMT techniques

** Compositional reasoning techniques

** Model simplification and recoding techniques

* An extended set of features

** Requirements Analysis

*** Property satisfiability

*** Property entailment

*** Unsatisfiable core extraction

*** Property realizability

** Dependability Assessment

*** Fault tree analysis

*** FMEA analysis

*** FDIR verification

*** Diagnosability checks