In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Property Value
dbo:abstract
  • In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code. The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic. (en)
  • Verifizierung oder Verifikation (von lat. veritas ‚Wahrheit‘ und facere ‚machen‘) ist der Nachweis, dass ein vermuteter oder behaupteter Sachverhalt wahr ist. Der Begriff wird unterschiedlich gebraucht, je nachdem, ob man sich bei der Wahrheitsfindung nur auf einen geführten Beweis stützen mag oder aber auch die in der Praxis leichter realisierbare bestätigende Überprüfung und Beglaubigung des Sachverhaltes durch Argumente einer unabhängigen Instanz als Verifizierung betrachtet. (de)
  • La verificación formal es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica), en el que partiendo de un conjunto axiomático, reglas de inferencia y algún lenguage lógico (como la lógica de primer orden u otra de preferencia una lógica sólida y completa), se puede encontrar una demostración o prueba de corrección de un programa. (es)
  • On parle de vérification formelle quand on utilise les techniques des méthodes formelles. Se référer à cet article pour plus de détails. Dans le monde industriel, la vérification formelle est utilisée aussi bien pour vérifier du code informatique, que du code de circuits électroniques. * Portail de l’informatique Portail de l’informatique * Portail de l'informatique théorique Portail de l'informatique théorique (fr)
  • 形式的検証(けいしきてきけんしょう)とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。 “”—ACMシンポジウムで発表された論文の要約から (ja)
  • Weryfikacja formalna – stwierdzenie poprawności algorytmu w oparciu o formalne metody matematyczne. (pl)
  • Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais. (pt)
  • Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы. (ru)
  • 在计算机硬件(特别是集成电路)和软件系统的设计过程中,形式验证的含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。 (zh)
dbo:wikiPageID
  • 270054 (xsd:integer)
dbo:wikiPageRevisionID
  • 740300401 (xsd:integer)
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • Verifizierung oder Verifikation (von lat. veritas ‚Wahrheit‘ und facere ‚machen‘) ist der Nachweis, dass ein vermuteter oder behaupteter Sachverhalt wahr ist. Der Begriff wird unterschiedlich gebraucht, je nachdem, ob man sich bei der Wahrheitsfindung nur auf einen geführten Beweis stützen mag oder aber auch die in der Praxis leichter realisierbare bestätigende Überprüfung und Beglaubigung des Sachverhaltes durch Argumente einer unabhängigen Instanz als Verifizierung betrachtet. (de)
  • La verificación formal es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica), en el que partiendo de un conjunto axiomático, reglas de inferencia y algún lenguage lógico (como la lógica de primer orden u otra de preferencia una lógica sólida y completa), se puede encontrar una demostración o prueba de corrección de un programa. (es)
  • On parle de vérification formelle quand on utilise les techniques des méthodes formelles. Se référer à cet article pour plus de détails. Dans le monde industriel, la vérification formelle est utilisée aussi bien pour vérifier du code informatique, que du code de circuits électroniques. * Portail de l’informatique Portail de l’informatique * Portail de l'informatique théorique Portail de l'informatique théorique (fr)
  • 形式的検証(けいしきてきけんしょう)とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。 “”—ACMシンポジウムで発表された論文の要約から (ja)
  • Weryfikacja formalna – stwierdzenie poprawności algorytmu w oparciu o formalne metody matematyczne. (pl)
  • Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais. (pt)
  • Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы. (ru)
  • 在计算机硬件(特别是集成电路)和软件系统的设计过程中,形式验证的含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。 (zh)
  • In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code. (en)
rdfs:label
  • Formal verification (en)
  • Verifizierung (de)
  • Verificación formal (es)
  • Vérification formelle (fr)
  • 形式的検証 (ja)
  • Weryfikacja formalna (pl)
  • Verificação formal (pt)
  • Формальная верификация (ru)
  • 形式验证 (zh)
owl:differentFrom
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:academicDiscipline of
is dbo:genre of
is dbo:knownFor of
is dbo:mainInterest of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbp:paradigm of
is dbp:typing of
is foaf:primaryTopic of