About: KeY

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: KeY Goto Sponge NotDistinct Permalink

An Entity of Type : umbel-rc:SoftwareObject, within Data Space : dbpedia.org associated with source document(s)
QRcode icon

http://dbpedia.org/describe/?url=http%3A%2F%2Fdbpedia.org%2Fresource%2FKeY

The KeY tool is used in formal verification of Java programs. It accepts specifications written in the Java Modeling Language to Java source files. These are transformed into theorems of dynamic logic and then compared against program semantics that are likewise defined in terms of dynamic logic. KeY is significantly powerful in that it supports both interactive (i.e. by hand) and fully automated correctness proofs. Failed proof attempts can be used for a more efficient debugging or verification-based testing. There have been several extensions to KeY in order to apply it to the verification of C programs or hybrid systems. KeY is jointly developed by Karlsruhe Institute of Technology, Germany; Technische Universität Darmstadt, Germany; and Chalmers University of Technology in Gothenburg,

Attributes	Values
rdf:type	Thing software schema:CreativeWork work wikidata:Q386724 Software umbel-rc:SoftwareObject
rdfs:label	KeY (logiciel) (fr) KeY (en)
rdfs:comment	Le logiciel KeY est un outil de vérification formelle de programmes Java. Débuté en 1998, le projet KeY est porté par l'Institut de technologie de Karlsruhe, l'Université de technologie de Darmstadt et l'École polytechnique Chalmers. KeY accepte les spécifications écrites à l'aide du Java Modeling Language (JML). (fr) The KeY tool is used in formal verification of Java programs. It accepts specifications written in the Java Modeling Language to Java source files. These are transformed into theorems of dynamic logic and then compared against program semantics that are likewise defined in terms of dynamic logic. KeY is significantly powerful in that it supports both interactive (i.e. by hand) and fully automated correctness proofs. Failed proof attempts can be used for a more efficient debugging or verification-based testing. There have been several extensions to KeY in order to apply it to the verification of C programs or hybrid systems. KeY is jointly developed by Karlsruhe Institute of Technology, Germany; Technische Universität Darmstadt, Germany; and Chalmers University of Technology in Gothenburg, (en)
foaf:name	KeY (en)
foaf:homepage	https://www.key-project.org/
name	KeY (en)
foaf:depiction
dcterms:subject	Formal methods tools Free theorem provers Proof assistants
Wikipage page ID	12528650 (xsd:integer)
Wikipage revision ID	1076362210 (xsd:integer)
Link from a Wikipage to another Wikipage	Carnegie Mellon University MISRA C Deductive reasoning Formal methods tools Homophone Hybrid systems University of Oldenburg Debugging Dynamic logic (modal logic) Mathematica GNU General Public License Control flow Symbolic execution C (programming language) Duality (mathematics) ETH Zürich Eclipse (software) First-order logic Formal verification Java (programming language) Technische Universität Darmstadt Hybrid system Free theorem provers Proof assistants Chalmers University of Technology Chimera (mythology) Karlsruhe Institute of Technology KeY Java Modeling Language Automated theorem prover Termination analysis Springer International Publishing Springer Science+Business Media C programming language Sequent calculus Model-based testing Weakest precondition Formal logic Java web start Hoare calculus Kripke structure Abstract State Machine Unit tests
Link from a Wikipage to an external page	http://vstte.ethz.ch/Files/stump.pdf http://www.ls.cs.cmu.edu/KeYmaeraX/ https://www.key-project.org/ http://www.dwheeler.com/essays/high-assurance-floss.html http://symbolaris.com/logic/dL.html http://www.key-project.org https://doi.org/10.1007%2Fs00165-008-0084-5 https://www.springer.com/978-3-319-49811-9 https://www.springer.com/east/home/generic/search/results%3FSGWID=5-40109-22-173712406-0 http://symbolaris.com/info/KeYmaera.html
sameAs	KeY KeY KeY KeY
dbp:wikiPageUsesTemplate	dbt:Commons_category dbt:ISBN dbt:Infobox_software dbt:Main dbt:More_footnotes dbt:Multiple_issues dbt:Reflist dbt:Release_date dbt:Jargon
thumbnail	wiki-commons:Special:FilePath/KeY_logo.svg?width=300
caption	Screenshot of KeY 1.4 (en)
developer	Technische Universität Darmstadt Chalmers University of Technology Karlsruhe Institute of Technology
genre	Formal verification
language	English (en)
latest release date	2020-12-18 (xsd:date)
latest release version	2.800000 (xsd:double)
license	GNU General Public License
logo	KeY logo.svg (en)

Faceted Search & Find service v1.17_git139 as of Feb 29 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3330 as of Mar 19 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (378 GB total memory, 60 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software