• PolyBoRi

  • Referenced in 48 articles [sw00723]
  • software verification based on Boolean expressions, which suffer-besides from the complexity of the problems...
  • KeYmaera

  • Referenced in 42 articles [sw03709]
  • notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable ... hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier...
  • FunFrog

  • Referenced in 6 articles [sw06571]
  • approximation of function calls. In every successful verification run, FunFrog generates function summaries ... reuses them to reduce the complexity of the successive verification. To prevent reporting spurious errors...
  • Isabelle/Circus

  • Referenced in 13 articles [sw15208]
  • Specification and Verification Environment. The Circus specification language combines elements for complex data and behavior...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • devices interacting with the physical environment. The complexity of such systems makes the design very ... infinite-state systems to the verification of complex embedded systems design. HYDI extends the standard...
  • Breach

  • Referenced in 24 articles [sw20822]
  • Breach, a toolbox for verification and parameter synthesis of hybrid systems. We describe Breach ... embedded systems design to the analysis of complex non-linear models from systems biology...
  • Aximo

  • Referenced in 4 articles [sw15031]
  • theoretical result: the worst case complexity of the verification problem of Aximo...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • WoLFram is successfully applied to the verification of PLC programs. Equivalence checking and property checking ... computational overhead is moderate. For more complex software run time limitations may occur. Replacing...
  • HIP

  • Referenced in 27 articles [sw09786]
  • separation logic based automated verification system for a simple imperative language, able to modularly verify ... user defined inductive predicates used to model complex data structures. Specifications can contain both heap...
  • JBernstein

  • Referenced in 2 articles [sw19486]
  • analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures ... still a major obstacle for formal verification of real-world applications...
  • CAMPY

  • Referenced in 1 article [sw21704]
  • Complexity verification using guided theorem enumeration. Determining if a given program satisfies a given bound ... this work, we introduce an automatic verification algorithm, {sc Campy}, that determines if a given ... platforms satisfy or do not satisfy expected complexity bounds...
  • Galculator

  • Referenced in 5 articles [sw09979]
  • device to tackle the complexity of proofs in program verification. The paper describes the architecture...
  • QuickChick

  • Referenced in 5 articles [sw13283]
  • same underlying verification methodology. We also apply this methodology to a complex case study...
  • Reveal

  • Referenced in 20 articles [sw00801]
  • describe the Reveal formal functional verification system and its application to four representative hardware test ... CEGAR, and is suitable for verifying the complex control logic of designs with wide datapaths ... this system, we believe that automating the verification for a useful class of hardware designs...
  • SCR

  • Referenced in 19 articles [sw06939]
  • tables, eliminate their ambiguous semantics, facilitate the verification and validation process, and improve the toolset ... extension is simple and avoids the complexity of temporal logic...
  • Torsche

  • Referenced in 4 articles [sw05038]
  • used for a complex scheduling algorithms design and verification. Therefore, our main goal...
  • FLAVERS

  • Referenced in 4 articles [sw09079]
  • state verification technique for software systems. Software systems are increasing in size and complexity ... alternative to testing and to formal verification approaches based on theorem proving. There has recently ... scale adequately to handle the complexity usually found in software. In this paper, we describe...
  • MFIX-DEM

  • Referenced in 9 articles [sw18199]
  • flows. In this paper, a series of verification cases is employed which tests the different ... extensively verified code as the physics is complex with highly-nonlinear coupling ... accuracy of the results without rigorous verification. These series of verification tests set the stage...
  • dSPIN

  • Referenced in 31 articles [sw09888]
  • checker that offers efficient means for the verification of concurrent programs written in high ... existing modeling techniques, while coping with potential complexity blow-ups caused by adding extra functionalities...
  • Ligero

  • Referenced in 5 articles [sw28502]
  • whose communication complexity is proportional to the square-root of the verification circuit size...