• KIDS

  • Referenced in 12 articles [sw15441]
  • development of correct and efficient programs from formal specifications, is described. The system has components ... performing algorithm design, deductive inference, program simplification, partial evaluation, finite differencing optimizations, data type refinement...
  • OFMC

  • Referenced in 28 articles [sw09466]
  • transition system resulting from an IF specification. OFMC’s effectiveness is due to the integration ... symbolic, constraint-based techniques, which are correct and terminating. The two major techniques ... integrates the lazy intruder with ideas from partial-order reduction. Moreover, OFMC allows...
  • Synthia

  • Referenced in 8 articles [sw12933]
  • given system is correct by providing a correctness certificate to the user. Such certificates ... reflect the specification-critical properties of the system. Synthia can also handle partially implemented systems...
  • PINNsNTK

  • Referenced in 25 articles [sw42058]
  • range of forward and inverse problems involving partial differential equations. However, despite their noticeable empirical ... width limit during training via gradient descent. Specifically, we derive the NTK of PINNs ... series of numerical experiments to verify the correctness of our theory and the practical effectiveness...
  • TRANSIT

  • Referenced in 6 articles [sw28674]
  • programmer to describe the desired system partially using the traditional model of communicating extended finite ... execution fragments that describe the correct behavior in the specific scenario corresponding to the counterexample ... language and prototype implementation of the proposed specification methodology for distributed protocols. Experimental evaluations ... seconds, a complete implementation from a specification consisting of the EFSM structure...
  • TRIM

  • Referenced in 7 articles [sw01375]
  • with capabilities for expressing conditional and partial behavior and with amathematically precise notion of refinement ... used to check whether oneset of requirements correctly elaborates on another. This paper presents TRIM ... routine forchecking refinements among TMSC specifications; and (iii) a capability for generatingdiagnostic information...
  • GOAL

  • Referenced in 7 articles [sw21229]
  • automata and temporal logic formulae. It also partially supports other variants of omega-automata ... also be used to construct correct and smaller specification automata, supplementing model checkers such...
  • CPBPV

  • Referenced in 5 articles [sw00164]
  • uses constraint stores to represent both the specification and the program and explores execution paths ... properties exists. The input program is partially correct under the boundness restrictions, if each constraint...
  • DynAlloy

  • Referenced in 3 articles [sw39829]
  • present DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems ... syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation ... tool in such a way that DynAlloy specifications are also automatically analyzable, as standard Alloy...
  • PSync

  • Referenced in 5 articles [sw17450]
  • PSync: a partially synchronous language for fault-tolerant distributed algorithms. Fault-tolerant distributed algorithms play ... These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence ... computers crashing. We introduce PSync, a domain specific language based on the Heard-Of model ... programming language with a runtime system for partially synchronous networks. We show the applicability...
  • SAT Solver Verification

  • Referenced in 5 articles [sw28831]
  • solver descriptions are given and their partial correctness and termination is proved. These include ... solver with a specific conflict analysis algorithm (similar to the description given in (Krstic...
  • ETCH

  • Referenced in 3 articles [sw07636]
  • that the syntax of the model is correct, but performs only limited type checking ... detection of mismatched message arguments in Promela specifications that use dynamic channel passing. This ... because the types of channels are only partially specified in Promela. ETCH extends the type...
  • jPredictor

  • Referenced in 5 articles [sw23065]
  • order to achieve more relaxed causal partial order on events that are relevant ... prediction, while still keeps the correctness of the results. Essentially, if the tranditional causality ... control-flow/data-flow dependence among events. More specifically, only a part of the causality that...
  • mural

  • Referenced in 9 articles [sw23627]
  • version resulting from such a step is correct with respect to the previous version. Since ... Appendix C (88 pp) containing the complete specification of the proof assistant. The first ... predicate calculus and for a logic of partial functions. The next chapter is a very...
  • TAK

  • Referenced in 1 article [sw30693]
  • However, many of these analyses still require specific computing environments and/or moderate levels of knowledge ... both the relevant programming language and the correct way to take these fundamental building blocks ... efficient and effective topographic analysis. To partially address this, we have written the Topographic Analysis...
  • HCViewer

  • Referenced in 1 article [sw22147]
  • unreliable, and partially reliable bioimpedance body composition data has shown high diagnostic specificity ... with the correction for false alarm rate), and the high level of heterogeneity in data...
  • PPlan

  • Referenced in 2 articles [sw20685]
  • planner together with theoretical results on the correctness and optimality of the algorithm. The language ... component properties. A preference formula provides a partial order on what are effectively temporally extended ... takes as input, an action theory, a specification of the initial state of the system...
  • ATLAS

  • Referenced in 199 articles [sw00056]
  • This paper describes the Automatically Tuned Linear Algebra...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • BoomerAMG

  • Referenced in 200 articles [sw00086]
  • BoomerAMG: A parallel algebraic multigrid solver and preconditioner...