Diferencia entre revisiones de «Verificación de sistemas SAT»
(New page: El objetivo es construir en ACL2 un sistema SAT cuya eficiencia sea comparable a los más avanzados y formalmente verificado en ACL2.) |
|||
| Línea 1: | Línea 1: | ||
| − | El objetivo es construir en ACL2 un sistema SAT | + | El objetivo es construir en ACL2 un sistema SAT con un doble objetivo |
| + | # la eficiencia del sistema debe de ser comparable con los más avanzados y | ||
| + | # las propiedades crítica del sistema deben de verificarse formalmente en ACL2. | ||
| + | |||
| + | Como punto de partida se puede usar el siguiente trabajo | ||
| + | : {{fmartin}}, {{jalonso}}, {{mjoseh}}, {{jruiz}}: ''Formal Verification of a Generic Framework to Synthesize SAT-Provers.'' Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313. | ||
| + | donde se muestra la construcción de un sistema SAT basado en DPLL. | ||
| + | |||
| + | Otro trabajo interesante para el proyecto es | ||
| + | : Filip Maric [http://afp.sourceforge.net/entries/SATSolverVerification.shtml Formal Verification of Modern SAT Solvers]. The Archive of Formal Proofs, 2008-07-23. | ||
| + | donde verifica en Isabelle propiedades de sistemas SAT. El trabajo es interesante desde el punto de vista de las demostraciones, pero carece de algoritmos ejecutables. | ||
| + | : | ||
Revisión del 21:19 22 oct 2008
El objetivo es construir en ACL2 un sistema SAT con un doble objetivo
- la eficiencia del sistema debe de ser comparable con los más avanzados y
- las propiedades crítica del sistema deben de verificarse formalmente en ACL2.
Como punto de partida se puede usar el siguiente trabajo
- Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina: Formal Verification of a Generic Framework to Synthesize SAT-Provers. Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313.
donde se muestra la construcción de un sistema SAT basado en DPLL.
Otro trabajo interesante para el proyecto es
- Filip Maric Formal Verification of Modern SAT Solvers. The Archive of Formal Proofs, 2008-07-23.
donde verifica en Isabelle propiedades de sistemas SAT. El trabajo es interesante desde el punto de vista de las demostraciones, pero carece de algoritmos ejecutables.
