Project Tags: Software Engineering and Logic

Minicomplexity

Computational Complexity Theory studies the fundamental properties of computation, independent of computational model. Many of its open questions are by now long-standing, having already defied decades of intense attacks by…

Automating the meta-theory of proof systems

Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious…

Automated verification of properties of concurrent, distributed and parallel specifications with applications to computer security

With NPRP project 09-1107-1-168 (ending in February 2014), we have outlined the foundations of a framework for representing Concurrent, Distributed and Parallel (CDP) languages and explored methodologies to formally prove…

Model-driven engineering of service-oriented process-based software systems

Service-oriented Computing (SOC) gained tremendous interest by the academic and industrial communities in the last decade. Nowadays, several business software systems are developed based on that paradigm. As opposed to…

Effective parallel and distributed programming via join pattern with guards, propagation and more

Recent advances in distributed systems and multicore architectures, and the emerging interest in Cloud Computing has unleashed significant pressures upon the programming language community to research and develop better general…

Reimplementing dependent pattern matching and termination checking in the Coq theorem prover

Coq is an interactive proof assistant (theorem prover) based on a long-studied dependent Type Theory called the Calculus of (Co-)Inductive Constructions (CIC). It is a mature system that has been…

Usable automated data inference for end-users

Nowadays, data are more easily accessible than ever, yet support for correlating base data into interesting consequences is often unavailable, or too expensive, or too technical for many users. Lacking…

Alice for Middle East — Alice ME

Alice is a software tool for introducing computational thinking and programming concepts in the context of creating 3D animations. Alice has been remarkably successful in North America, where research has…

A type-safe programming language to build safe and secure web applications

Software as a Service (SaaS) is the idea of pushing software and data from the desktop to the Web. For instance, Google Docs is an office suite that is accessible…

Formal reasoning about languages for distributed computation

Foundational research in programming language semantics has given us the ability to design languages for sequential programming with strong theoretical properties, which translate into run-time assurance for programs written in…