|
|
|
|
|
|
Date Reviewed |
|
|
1 - 9 of 9
reviews
|
|
|
|
|
|
|
|
Verification methods for the computationally complete symbolic attacker based on indistinguishability Bana G., Chadha R., Eeralla A., Okada M. ACM Transactions on Computational Logic 21(1): 1-44, 2019. Type: Article
First-order logic formalization for security protocols and attackers enables formal verification. Once a formalization is established, standard tools such as a theorem prover can be used in the analysis....
|
Dec 16 2019 |
|
|
|
|
|
|
Modularisation of sequent calculi for normal and non-normal modalities Lellmann B., Pimentel E. ACM Transactions on Computational Logic 20(2): 1-46, 2019. Type: Article
Mathematician and logician Gerhard Gentzen introduced sequent calculus, a logical framework, in the first half of the 20th century. It can be used to establish systems for propositional, first-order, and modal logics. For the latter, i...
|
Oct 10 2019 |
|
|
|
|
|
|
Designing a semantic model for a wide-spectrum language with concurrency Colvin R., Hayes I., Meinicke L. Formal Aspects of Computing 29(5): 853-875, 2017. Type: Article
A concurrent wide-spectrum language combines a concurrent programming language with specification constructs. Colvin et al. provide a unified framework for defining the semantics of such languages. The semantics is trace-based and capt...
|
Jan 10 2018 |
|
|
|
|
|
|
The logical view on continuous Petri nets Blondin M., Finkel A., Haase C., Haddad S. ACM Transactions on Computational Logic 18(3): 1-28, 2017. Type: Article
The reachability problem for standard Petri nets is EXPSPACE hard, and the coverability problem is EXPSPACE complete. However, more efficient algorithms exist for variants of the standard nets. Continuous Petri nets are such a variant ...
|
Nov 17 2017 |
|
|
|
|
|
|
Argumentation update in YALLA (yet another logic language for argumentation) Dupin de Saint-Cyr F., Bisquert P., Cayrol C., Lagasquie-Schiex M. International Journal of Approximate Reasoning 75(C): 57-92, 2016. Type: Article
“Bob murdered Alice” and “Bob did not murder Alice” are two arguments....
|
Sep 12 2016 |
|
|
|
|
|
|
Exploring cognitive style and task-specific preferences for process representations Figl K., Recker J. Requirements Engineering 21(1): 63-85, 2016. Type: Article
Modeling a business process can help one understand the process; it can also be used to communicate the process. Later on, the model can be used to execute the process, to derive a software implementation for it, or to enhance the proc...
|
Jun 20 2016 |
|
|
|
|
|
|
Accelerating worst case execution time analysis of timed automata models with cyclic behaviour Al-Bataineh O., Reynolds M., French T. Formal Aspects of Computing 27(5-6): 917-949, 2015. Type: Article
The worst-case execution time (WCET) is an important property of safety-critical systems. In general, a safety-critical system can be analyzed using a formal model. An established formalism for modeling such systems is a timed automato...
|
Mar 31 2016 |
|
|
|
|
|
|
A method and tool for tracing requirements into specifications Hallerstede S., Jastram M., Ladenberger L. Science of Computer Programming 822-21, 2014. Type: Article
Formalizing informal specifications requires traceability. System descriptions are rarely fully formalized right from the start. Assumptions on the environment and requirements of the system are often specified semi-formally or as a mi...
|
Oct 22 2014 |
|
|
|
|
|
|
On the relative strength of pebbling and resolution Nordström J. ACM Transactions on Computational Logic 13(2): 1-43, 2012. Type: Article
Resolution refutation can beat black-only pebbling. This is the main result of this paper....
|
Jul 9 2012 |
|
|
|
|
|
|
|
|
|
|
|