Lecturas del Grupo de Lógica Computacional (Agosto de 2011)
Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de agosto de 2011.
La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
- Theorem proving for verification (the early days) #Historia
- Selecting attributes for sport forecasting using formal concept analysis #AFC
- Lecturas del Grupo de Lógica Computacional (Julio de 2011). #GLC #Vestigium
- Formal methods: practice and experience #Métodos_formales
- Automated deduction for verification #DAT
- Software model checking #Model_checking
- The verified software initiative: A Manifesto #Verificación
- How can i do that with ACL2 recent enhancements to ACL2 #ACL2
- Algebraic proofs over noncommutative formulas #Cálculo_polinomial
- Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
- Formalization of an Efficient Representation of Bernstein Polynomials and Applications to Global Optimization #PVS
- Automating Algebraic Methods in Isabelle #Isabelle
- A Repository for Tarski-Kleene Algebras #Isabelle
- Emergence and refinement #Emergencia #Refinamentos
- Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL #Isabelle
- How Efficient Can Fully Verified Functional Programs Be – A Case Study of Graph Traversal Algorithms #Isabelle
- Imperative functional programming with Isabelle/HOL #Isabelle
- A Flexible Formal Verification Framework for Industrial Scale Validation #ACL2
- Markets are Efficient if and Only if P = NP.
- Bit-Blasting ACL2 Theorems #ACL2 #GL
- A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. #ACL2 #GL
- Integrating Testing and Interactive Theorem Proving #ACL2
- seL4 Enforces Integrity #Isabelle
- Peirce’s Truth-functional Analysis and the Origin of Truth Tables. #Historia
- Towards Flight Control Verification Using Automated Theorem Proving #MetiTarski
- Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
- Lightweight Tools for Heavyweight Semantics. #Lem #Ott #Coq #Isabelle #HOL
- Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
- Maximum Cardinality Matching. #Isabelle
- Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. #AA
- Gauss-Jordan Elimination for Matrices Represented as Functions. #Isabelle
- Verification of Dependable Software using Spark and Isabelle. #Isabelle
- Verification of Programs in Virtual Memory Using Separation Logic. #Isabelle
- Automated Specification Analysis Using an Interactive Theorem Prover. #ACL2
- Formal Analysis of Fractional Order Systems in HOL. #HOL
En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.