
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, constraintbased techniques, which are correct and terminating. The two major techniques ... integrates the lazy intruder with ideas from partialorder 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 specificationcritical 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 omegaautomata ... 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 faulttolerant distributed algorithms. Faulttolerant 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 HeardOf 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 ... controlflow/dataflow 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...