• Isar

  • Referenced in 145 articles [sw04599]
  • abstraction for user-level work. The Isar formal proof language has been designed to satisfy ... integrates a broad range of automated proof methods. Interactive proof development is supported directly ... system provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either...
  • RRL

  • Referenced in 55 articles [sw28904]
  • automated reasoning literature as well as a research tool for investigating the use of formal ... methods in hardware and software design. We provide a brief historical account of development...
  • Korat

  • Referenced in 33 articles [sw07259]
  • automated testing of Java programs. Given a formal specification for a method, Korat uses...
  • JUnit

  • Referenced in 33 articles [sw07262]
  • checker to decide whether methods are working correctly, thus automating the writing of unit test ... writing testing code, the programmer writes formal specifications (e.g., pre- and postconditions). This makes...
  • Paramils

  • Referenced in 87 articles [sw00678]
  • this algorithm configuration problem. More formally, we provide methods for optimizing a target algorithm ... comprehensive experimental evaluation of our methods, based on the configuration of prominent complete and incomplete ... identified with considerable effort. Nevertheless, using our automated algorithm configuration procedures, we achieved substantial...
  • MPTP 0.2

  • Referenced in 53 articles [sw02589]
  • large formal Mizar Mathematical Library (MML) available to current first-order automated theorem provers (ATPs ... knowledge-based, and generally AI-based ATP methods. This version of MPTP switches ... Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • rewrite relations and its application to the automated verifications of termination certificates. Termination ... Turing-complete formalism of term rewriting. Over the years, many methods and tools have been ... also present its application to the automated verification of termination certificates, as produced by termination...
  • Lean

  • Referenced in 46 articles [sw15148]
  • automated theorem proving, by situating automated tools and methods in a framework that supports user ... systems. It is currently being used to formalize category theory, homotopy type theory, and abstract...
  • HOLyHammer

  • Referenced in 26 articles [sw11553]
  • upload and automatically process an arbitrary formal development (project) based on HOL Light ... service uses several automated reasoning systems combined with several premise selection methods trained...
  • VeriFun

  • Referenced in 10 articles [sw22187]
  • easy to use system for teaching Automated Reasoning, Semantics, Verification and similar subjects ... been used in beginner courses about Formal Methods as well as in practical courses about...
  • LATIN

  • Referenced in 16 articles [sw19699]
  • developing methods, techniques, and tools for interfacing logics and related formal systems. These systems ... implemented in systems like (semi-)automated theorem provers, model checkers, computer algebra systems, constraint solvers...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • long-term and large-scale formalization effort. MizarMode has been designed with ... code-searching” methods, and tools programmed or integrated within it. These methods and tools ... include, e.g., the automated generation of proof skeletons, semantic browsing of the articles and abstracts...
  • Krohn-Rhodes

  • Referenced in 4 articles [sw08794]
  • applications, such as automated object-oriented programming in software development, formal methods for understanding...
  • NAT2TEST

  • Referenced in 3 articles [sw16844]
  • formal modelling knowledge. Automation also allows an early application of formal methods within the software...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • natural deduction. It supports light-weight formal methods via compositional specification-based testing and bounded ... code. It is designed to support decidable automated reasoning, to improve proof stability...
  • GenProg

  • Referenced in 4 articles [sw22863]
  • automated method for repairing defects in off-the-shelf, legacy programs without formal specifications, program...
  • qFunctions

  • Referenced in 5 articles [sw30803]
  • recurrences, and formal substitutions. Here, we also extend the classical method of the weighted words ... approach. Moreover, qFunctions has implementations that automate the recurrence system creation of the weighted words...
  • Truth/SLC

  • Referenced in 8 articles [sw01623]
  • view of the inherent complexity of formal methods it is desirable to provide the user ... justifiable. There is one particularly successful automated approach to verification, called model checking, in which...
  • Loopy

  • Referenced in 1 article [sw40305]
  • Loopy: Programmable and Formally Verified Loop Transformations. This paper presents a system, Loopy, for programming ... tedious and error-prone, while fully automated methods do not guarantee improvements. Loopy takes ... then carried out automatically by Loopy, and formally verified to guard against specification and implementation ... offers considerable flexibility with assembling transformations, while automation and checking prevent errors. Loopy is implemented...
  • metaSMT

  • Referenced in 1 article [sw41584]
  • formal methods use decision procedures as their core solving engines. In this context, automated reasoning...