Pinned Repositories
acl-lean
A theorem prover for propositional access control logic with "says" operator. Implements Seq-ACL, an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs. Main implementation in SWI-Prolog with translation to GNU-Prolog and relative C bindings provided.
Azure
Azure misc. scripts & interesting bits
Azure-Batch
Batch code samples
budget-visualization
Visualize expenses against income by month and category.
cyclecloud-mclaren
CycleCloud templates with multiple "node arrays", for PBS and SLURM.
delegation2spass
A reducer and translator for a set of complete reduction axioms. Simplifies dynamic formulae for a delegation/revocation logic and converts them into propositional logic expressed in DFG syntax.
nesy
Neural-Symbolic Rule-Based Monitoring.
random-attack
Consensus in asynchronous networks with random faults.
secommunity
A collection of tools that can be used to define distributed access control policies using an extension of the Answer Set Programming system DLV. In particular, several external predicates were developed, which can be used via DLV-Complex, with the aim to query remote knowledge bases. A server that handles such queries using its own local DLV-Complex instance was also written in the context of this work.
seq-acl
A decidable theorem prover for the modal access control logic "ACL+". Implements an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs.
rispoli's Repositories
rispoli/secommunity
A collection of tools that can be used to define distributed access control policies using an extension of the Answer Set Programming system DLV. In particular, several external predicates were developed, which can be used via DLV-Complex, with the aim to query remote knowledge bases. A server that handles such queries using its own local DLV-Complex instance was also written in the context of this work.
rispoli/acl-lean
A theorem prover for propositional access control logic with "says" operator. Implements Seq-ACL, an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs. Main implementation in SWI-Prolog with translation to GNU-Prolog and relative C bindings provided.
rispoli/delegation2spass
A reducer and translator for a set of complete reduction axioms. Simplifies dynamic formulae for a delegation/revocation logic and converts them into propositional logic expressed in DFG syntax.
rispoli/nesy
Neural-Symbolic Rule-Based Monitoring.
rispoli/random-attack
Consensus in asynchronous networks with random faults.
rispoli/seq-acl
A decidable theorem prover for the modal access control logic "ACL+". Implements an analytic labeled sequent calculus for access control logic along with an automatic generation of human-readable proofs.
rispoli/Azure
Azure misc. scripts & interesting bits
rispoli/Azure-Batch
Batch code samples
rispoli/budget-visualization
Visualize expenses against income by month and category.
rispoli/cyclecloud-mclaren
CycleCloud templates with multiple "node arrays", for PBS and SLURM.
rispoli/dotfiles
Configuration files.
rispoli/interactive-realizers
An implementation of interactive realizers for classical arithmetic without nested quantifiers.
rispoli/isomorphism
A Prolog isomorphism checker for Intersection Types.
rispoli/luna
Provisioning tool for clusters
rispoli/macl2spass
A translator from policies written in modal access control logic (M-ACL) into first-order formulae expressed in DFG syntax. The resulting output can be directly used to reason about access control with the SPASS theorem prover.
rispoli/macl2thf
A translator from policies written in modal access control logic (M-ACL) into higher-order formulae expressed in THF0, the core of the TPTP language, based on Church's simple type theory. The resulting output can be directly used to reason about access control with one of the many higher order automated theorem provers and assistants available.
rispoli/misc-scripts
Little scripts collected or written through the years.
rispoli/nesy-hs
Neural-Symbolic Rule-Based Monitoring (Haskell version).
rispoli/opfpq
Optimal purely functional priority queues.
rispoli/pinterpreter
A π-calculus interpreter and type-checker.
rispoli/predict-remote
Client/server wrapper around the LIBLINEAR's Python interface.
rispoli/scwc
A Simulator for the Stochastic CWC.
rispoli/seq-tab
Sequent Calculus and Tableaux Resolution Method.
rispoli/smart-access
A platform for the development of secure applications in the context of cloud computing access control.
rispoli/trinity
ClusterVision OpenStack Trinity repository
rispoli/trinity_scripts
rispoli/txt2ws
Translate your ASCII files to a Whitespace program that outputs back your original text.