KindSoftware
  • about us
  • software
  • documents
  • research
  • visitors
  • cdes
  • blog
Documents
  • Overview
  • Mechanized Theory
    • Formalizing Feature Models
    • Verified Visualisation of Textual Modelling Languages
    • The Concurrency Semantic Property
  • News
    • 2011
    • 2010
    • 2009
    • 2008
    • 2007
    • 2006
    • 2005
    • 2004
    • 2003
  • Project Proposals
    • Programing and Specification Languages
    • IDEs
    • Theory
    • Operating Systems and Compilers
    • Theorem Provers
    • Verification
    • Case Studies
  • Published Papers
  • Reports
  • Talks
    • December 2011 - Validating Semantics
    • Throughout 2011 - Democracy as a Critical System
    • April 2011 - Reasoning about Concurrency in (RT) Java
    • November 2010 - Student Group Work
    • May 2008 - Tool Integration
    • May 2008 - Secret Ninja Formal Methods
    • May 2008 - Verified Gaming
    • May 2008 - The Mobius Program Verification Environment
    • April 2008 - A Bit of Rigor
    • 2007 - Practical Verification of Java
    • 2007 - KeY Symposium
    • September 2007 - SAVCBS
    • September 2007 - SPLC
    • August 2007 - EVT
    • November 2006 - TGC
    • June 2006 - Odysseus
    • November 2005 - FMCO
    • July 2005 - FM GC6
    • June 2005 - KSU
    • December 2004 - AIST
    • August 2002 - LAJUG
  • Tutorials
    • ECOOP 2004
    • ETAPS 2005
    • FM 2005
    • ECOOP 2005
    • ESEC/FSE 2005
    • FMCO 2005
    • ETAPS 2008
    • TOOLS 2008
    • GLOBAN 2008
    • ETAPS 2009
    • COST 2009
  • White Papers
    • KindSoftware Coding Standards
    • Exercises from "Algebraic Semantics of Imperative Programs" Solutions

Formalizing Feature Models

This work formalizes feature models in PVS. It is accompanied by the article "Reasoning about Feature Models in Higher-Order Logic."

  • the PVS theory
  • our proofs

Copyright © 2007 KindSoftware. :: Page Last Updated: Monday, 02-Jan-2012 16:00:16 CET
Site Design and Photos by CAW :: XHTML, CSS.