rispoli Goto Github PK

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.

dotfiles

Configuration files.

interactive-realizers

An implementation of interactive realizers for classical arithmetic without nested quantifiers.

isomorphism

A Prolog isomorphism checker for Intersection Types.

luna

Provisioning tool for clusters

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.

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.

misc-scripts

Little scripts collected or written through the years.

nesy

Neural-Symbolic Rule-Based Monitoring.

nesy-hs

Neural-Symbolic Rule-Based Monitoring (Haskell version).

opfpq

Optimal purely functional priority queues.

pinterpreter

A π-calculus interpreter and type-checker.

predict-remote

Client/server wrapper around the LIBLINEAR's Python interface.

random-attack

Consensus in asynchronous networks with random faults.

scwc

A Simulator for the Stochastic CWC.

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.

seq-tab

Sequent Calculus and Tableaux Resolution Method.

smart-access

A platform for the development of secure applications in the context of cloud computing access control.

trinity

ClusterVision OpenStack Trinity repository

trinity_scripts

txt2ws

Translate your ASCII files to a Whitespace program that outputs back your original text.