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:
The following is an incomplete list of the provided features:
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.
Changed lines 1-2 from:
(:title Features :)
to:
(:title Documentation :)
Changed lines 4-5 from:
%rfloat height=100px% {$TopLevelUrl}/images/uc.gif
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
Changed lines 17-18 from:
** IC3
to:
** IC3 based algorithms
** K-liveness
Changed lines 20-22 from:
*** Reachability analysis guided by a regular expression

* New model checking algorithms for infinite state systems
to:
*** Reachability analysis and invariant checking guided by a regular expression

* 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:
** Discrete Requirements Analysis
*** Property satisfiability
*** Property entailment
*** Unsatisfiable core extraction
*** Property realizability
November 05, 2013, at 03:01 PM by 192.168.156.46 -
Added lines 35-37:
** Explicit FSM view generation
*** Dump in .xmi format
*** Subject to predicate abstraction
November 05, 2013, at 02:59 PM by 192.168.156.46 -
Changed lines 12-15 from:
* Model simplification and recoding techniques
** Range Recoding
** Free input propagation

to:
Added lines 35-37:
** Model simplification and recoding techniques
*** Range Recoding
*** Free input propagation
November 05, 2013, at 02:58 PM by 192.168.156.46 -
Deleted lines 35-39:

(:comment Some less important details
** Abstraction via AllSMT, and in combiation with BDDs
*** Refinement via Unsatisfiable Core and Interpolation
)
November 05, 2013, at 02:57 PM by 192.168.156.46 -
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
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
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
)

Changed line 47 from:
*** Property realizability
to:
*** Property realizability
October 31, 2013, at 03:45 PM by 192.168.156.43 -
Changed line 8 from:
* An extended language
to:
* An extended language for synchronous systems
Deleted line 9:
** new constructs to represent network of (hybrid-)automata (HyDi)
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
to:
** Discrete Requirements Analysis
Changed lines 35-41 from:
*** Property realizability
** Dependability Assessment
*** Fault tree analysis
*** FMEA analysis
*** FDIR verification
*** Diagnosability checks

to:
*** Property realizability
June 12, 2011, at 08:04 PM by 94.39.213.133 -
Added line 4:
%rfloat height=100px% {$TopLevelUrl}/images/uc.gif
June 12, 2011, at 07:47 PM by 94.39.213.133 -
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata (HyDy)
to:
** new constructs to represent network of (hybrid-)automata (HyDi)
June 12, 2011, at 07:47 PM by 94.39.213.133 -
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata
to:
** new constructs to represent network of (hybrid-)automata (HyDy)
June 12, 2011, at 04:29 PM by 94.39.213.133 -
Changed line 29 from:
* An extended set of features
to:
* An extended set of functionalities
June 12, 2011, at 04:10 PM by 94.39.213.133 -
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
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
Added lines 23-24:
*** Bounded Model Checking via SMT
*** Abstraction based
Added lines 27-28:
*** Range Recoding
*** Free input propagation
Added line 31:
*** Hybrid and Discrete
June 12, 2011, at 04:06 PM by 94.39.213.133 -
Changed line 8 from:
** support for the [[http://aiger|AIGER]] format;
to:
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format;
June 12, 2011, at 03:58 PM by 94.39.213.133 -
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