Decidability; Pi-calculus; Program verification; Security of data

PICNIC is a tool for verifying security properties of systems, namely non-interference properties of processes expressed as terms of the pi-calculus with two security levels and declassification primitives. More precisely, it checks whether inserting …