
Blanc, Régis

SCALA '15: "Sound Reasoning about Integral ..."
Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface
Régis Blanc and Viktor Kuncak
(EPFL, Switzerland)
We extend the Leon verification system for Scala with support for bitvector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved in SMT solving by developing a solverindependent interface to easily configure the backend of Leon. Our interface is based on the emerging SMTLIB standard for SMT solvers, and we release a Scala library offering full support for the latest version of the standard. We use the standard BigInt Scala library to represent mathematical integers, whereas we correctly model Int as 32bit integers. We ensure safety of arithmetic by checking for division by zero and correctly modeling division and modulo. We conclude with a performance comparison between the sound representation of Ints and the cleaner abstract representation using mathematical integers, and discuss the tradeoff involved.
@InProceedings{SCALA15p35,
author = {Régis Blanc and Viktor Kuncak},
title = {Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {3540},
doi = {10.1145/2774975.2774980},
year = {2015},
}
Publisher's Version
Article Search


Jonnalagedda, Manohar

SCALA '15: "FoldBased Fusion as a Library: ..."
FoldBased Fusion as a Library: A Generative Programming Pearl
Manohar Jonnalagedda and Sandro Stucki
(EPFL, Switzerland)
Fusion is a program optimisation technique commonly implemented using specialpurpose compiler support. In this paper, we present an alternative approach, implementing foldbased fusion as a standalone library. We use staging to compose operations on folds; the operations are partially evaluated away, yielding code that does not construct unnecessary intermediate data structures. The technique extends to partitioning and grouping of collections.
@InProceedings{SCALA15p41,
author = {Manohar Jonnalagedda and Sandro Stucki},
title = {FoldBased Fusion as a Library: A Generative Programming Pearl},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {4150},
doi = {10.1145/2774975.2774981},
year = {2015},
}
Publisher's Version
Article Search


Kneuss, Etienne

SCALA '15: "CounterExample Complete Verification ..."
CounterExample Complete Verification for HigherOrder Functions
Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak
(EPFL, Switzerland)
We present a verification procedure for pure higherorder functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counterexamples. The procedure reduces the analysis of higherorder programs to checking satisfiability of a sequence of quantifierfree formulas over theories such as algebraic data types, integer linear arithmetic, and uninterpreted function symbols, thus enabling the use of efficient satisfiability modulo theory (SMT) solvers. Our solution supports arbitrary function types and arbitrarily nested anonymous functions (which can be stored in data structures, passed as arguments, returned, and applied). Among the contributions of this work is supporting even those cases when anonymous functions cannot be statically traced back to their definition, ensuring completeness of the approach for finding counterexamples. We provide a proof of soundness and counterexample completeness for our system as well as initial evaluation in the Leon verifier.
@InProceedings{SCALA15p18,
author = {Nicolas Voirol and Etienne Kneuss and Viktor Kuncak},
title = {CounterExample Complete Verification for HigherOrder Functions},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1829},
doi = {10.1145/2774975.2774978},
year = {2015},
}
Publisher's Version
Article Search


Kuncak, Viktor 
SCALA '15: "CounterExample Complete Verification ..."
CounterExample Complete Verification for HigherOrder Functions
Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak
(EPFL, Switzerland)
We present a verification procedure for pure higherorder functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counterexamples. The procedure reduces the analysis of higherorder programs to checking satisfiability of a sequence of quantifierfree formulas over theories such as algebraic data types, integer linear arithmetic, and uninterpreted function symbols, thus enabling the use of efficient satisfiability modulo theory (SMT) solvers. Our solution supports arbitrary function types and arbitrarily nested anonymous functions (which can be stored in data structures, passed as arguments, returned, and applied). Among the contributions of this work is supporting even those cases when anonymous functions cannot be statically traced back to their definition, ensuring completeness of the approach for finding counterexamples. We provide a proof of soundness and counterexample completeness for our system as well as initial evaluation in the Leon verifier.
@InProceedings{SCALA15p18,
author = {Nicolas Voirol and Etienne Kneuss and Viktor Kuncak},
title = {CounterExample Complete Verification for HigherOrder Functions},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1829},
doi = {10.1145/2774975.2774978},
year = {2015},
}
Publisher's Version
Article Search
SCALA '15: "Sound Reasoning about Integral ..."
Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface
Régis Blanc and Viktor Kuncak
(EPFL, Switzerland)
We extend the Leon verification system for Scala with support for bitvector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved in SMT solving by developing a solverindependent interface to easily configure the backend of Leon. Our interface is based on the emerging SMTLIB standard for SMT solvers, and we release a Scala library offering full support for the latest version of the standard. We use the standard BigInt Scala library to represent mathematical integers, whereas we correctly model Int as 32bit integers. We ensure safety of arithmetic by checking for division by zero and correctly modeling division and modulo. We conclude with a performance comparison between the sound representation of Ints and the cleaner abstract representation using mathematical integers, and discuss the tradeoff involved.
@InProceedings{SCALA15p35,
author = {Régis Blanc and Viktor Kuncak},
title = {Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {3540},
doi = {10.1145/2774975.2774980},
year = {2015},
}
Publisher's Version
Article Search


Métrailler, Christopher

SCALA '15: "ESPeciaL: An Embedded Systems ..."
ESPeciaL: An Embedded Systems Programming Language
Christopher Métrailler and PierreAndré Mudry
(University of Applied Sciences Western Switzerland, Switzerland)
The advent of offtheshelf programmable embedded systems such as Arduino enables people with little programming skills to interact with the realworld using sensors and actuators. In this paper, we propose a novel approach aimed at simplifying the programming of embedded systems based on the dataflow paradigm. Named ESPeciaL, this programming framework removes the need of lowlevel programming in C/C++, as the application is written by connecting blocks that produce and consume data. Thus, an embedded application can be described in terms of readytouse blocks that correspond to the various microcontroller peripherals and to program function (multiplexers, logic gates, etc.). The user application itself is written as an embedded Scala DSL. From that code, the ESPeciaL compiler then generates the corresponding C++ code which can be tailored  using different backends  to match different embedded systems or a QEMUbased simulation environment. To demonstrate the validity of the approach, we present a typical embedded systems application implemented using ESPeciaL
@InProceedings{SCALA15p51,
author = {Christopher Métrailler and PierreAndré Mudry},
title = {ESPeciaL: An Embedded Systems Programming Language},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {5155},
doi = {10.1145/2774975.2774982},
year = {2015},
}
Publisher's Version
Article Search


Milthorpe, Josh 
SCALA '15: "Distributed Programming in ..."
Distributed Programming in Scala with APGAS
Philippe Suter, Olivier Tardieu, and Josh Milthorpe
(IBM Research, USA)
APGAS (Asynchronous Partitioned Global Address Space) is a model for concurrent and distributed programming, known primarily as the foundation of the X10 programming language. In this paper, we present an implementation of this model as an embedded domainspecific language for Scala. We illustrate common usage patterns and contrast with alternative approaches available to Scala programmers. In particular, using two distributed algorithms as examples, we illustrate how APGASstyle programs compare to idiomatic Akka implementations. We demonstrate the use of APGAS places and tasks, distributed termination, and distributed objects.
@InProceedings{SCALA15p13,
author = {Philippe Suter and Olivier Tardieu and Josh Milthorpe},
title = {Distributed Programming in Scala with APGAS},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1317},
doi = {10.1145/2774975.2774977},
year = {2015},
}
Publisher's Version
Article Search


Mudry, PierreAndré 
SCALA '15: "ESPeciaL: An Embedded Systems ..."
ESPeciaL: An Embedded Systems Programming Language
Christopher Métrailler and PierreAndré Mudry
(University of Applied Sciences Western Switzerland, Switzerland)
The advent of offtheshelf programmable embedded systems such as Arduino enables people with little programming skills to interact with the realworld using sensors and actuators. In this paper, we propose a novel approach aimed at simplifying the programming of embedded systems based on the dataflow paradigm. Named ESPeciaL, this programming framework removes the need of lowlevel programming in C/C++, as the application is written by connecting blocks that produce and consume data. Thus, an embedded application can be described in terms of readytouse blocks that correspond to the various microcontroller peripherals and to program function (multiplexers, logic gates, etc.). The user application itself is written as an embedded Scala DSL. From that code, the ESPeciaL compiler then generates the corresponding C++ code which can be tailored  using different backends  to match different embedded systems or a QEMUbased simulation environment. To demonstrate the validity of the approach, we present a typical embedded systems application implemented using ESPeciaL
@InProceedings{SCALA15p51,
author = {Christopher Métrailler and PierreAndré Mudry},
title = {ESPeciaL: An Embedded Systems Programming Language},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {5155},
doi = {10.1145/2774975.2774982},
year = {2015},
}
Publisher's Version
Article Search


Prémont, Patrick

SCALA '15: "Referential Integrity with ..."
Referential Integrity with Scala Types
Patrick Prémont
(BoldRadius Solutions, Canada)
Referential integrity constraints are critical elements of relational data models, and have found widespread use in industry. However, their benefits in terms of data integrity do not fully extend to program correctness. Constraint violations are identified at runtime and must then be handled appropriately by programs. We show how Scala can be used to build data models and programs where referential integrity is enforced at compiletime. Scala’s type system, with its variance annotations and pathdependent types, is especially suited to express these constraints and proofs in a natural manner. We also explore potential compiler improvements that could enhance support for typechecked referential integrity.
@InProceedings{SCALA15p30,
author = {Patrick Prémont},
title = {Referential Integrity with Scala Types},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {3034},
doi = {10.1145/2774975.2774979},
year = {2015},
}
Publisher's Version
Article Search


Prokopec, Aleksandar 
SCALA '15: "SnapQueue: LockFree Queue ..."
SnapQueue: LockFree Queue with Constant Time Snapshots
Aleksandar Prokopec
(EPFL, Switzerland)
We introduce SnapQueues  concurrent, lockfree queues with a linearizable, lockfree globalstate transition operation. This transition operation can atomically switch between arbitrary SnapQueue states, and is used by enqueue, dequeue, snapshot and concatenation operations. We show that implementing these operations efficiently depends on the persistent data structure at the core of the SnapQueue. This immutable support data structure is an interchangeable kernel of the SnapQueue, and drives its performance characteristics. The design allows reasoning about concurrent operation running time in a functional way, absent from concurrency considerations. We present a support data structure that enables O(1) queue operations, O(1) snapshot and O(log n) atomic concurrent concatenation. We show that the SnapQueue enqueue operation achieves up to 25% higher performance, while the dequeue operation has performance identical to standard lockfree concurrent queues.
@InProceedings{SCALA15p1,
author = {Aleksandar Prokopec},
title = {SnapQueue: LockFree Queue with Constant Time Snapshots},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {112},
doi = {10.1145/2774975.2774976},
year = {2015},
}
Publisher's Version
Article Search


Stucki, Sandro

SCALA '15: "FoldBased Fusion as a Library: ..."
FoldBased Fusion as a Library: A Generative Programming Pearl
Manohar Jonnalagedda and Sandro Stucki
(EPFL, Switzerland)
Fusion is a program optimisation technique commonly implemented using specialpurpose compiler support. In this paper, we present an alternative approach, implementing foldbased fusion as a standalone library. We use staging to compose operations on folds; the operations are partially evaluated away, yielding code that does not construct unnecessary intermediate data structures. The technique extends to partitioning and grouping of collections.
@InProceedings{SCALA15p41,
author = {Manohar Jonnalagedda and Sandro Stucki},
title = {FoldBased Fusion as a Library: A Generative Programming Pearl},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {4150},
doi = {10.1145/2774975.2774981},
year = {2015},
}
Publisher's Version
Article Search


Suter, Philippe 
SCALA '15: "Distributed Programming in ..."
Distributed Programming in Scala with APGAS
Philippe Suter, Olivier Tardieu, and Josh Milthorpe
(IBM Research, USA)
APGAS (Asynchronous Partitioned Global Address Space) is a model for concurrent and distributed programming, known primarily as the foundation of the X10 programming language. In this paper, we present an implementation of this model as an embedded domainspecific language for Scala. We illustrate common usage patterns and contrast with alternative approaches available to Scala programmers. In particular, using two distributed algorithms as examples, we illustrate how APGASstyle programs compare to idiomatic Akka implementations. We demonstrate the use of APGAS places and tasks, distributed termination, and distributed objects.
@InProceedings{SCALA15p13,
author = {Philippe Suter and Olivier Tardieu and Josh Milthorpe},
title = {Distributed Programming in Scala with APGAS},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1317},
doi = {10.1145/2774975.2774977},
year = {2015},
}
Publisher's Version
Article Search


Tardieu, Olivier

SCALA '15: "Distributed Programming in ..."
Distributed Programming in Scala with APGAS
Philippe Suter, Olivier Tardieu, and Josh Milthorpe
(IBM Research, USA)
APGAS (Asynchronous Partitioned Global Address Space) is a model for concurrent and distributed programming, known primarily as the foundation of the X10 programming language. In this paper, we present an implementation of this model as an embedded domainspecific language for Scala. We illustrate common usage patterns and contrast with alternative approaches available to Scala programmers. In particular, using two distributed algorithms as examples, we illustrate how APGASstyle programs compare to idiomatic Akka implementations. We demonstrate the use of APGAS places and tasks, distributed termination, and distributed objects.
@InProceedings{SCALA15p13,
author = {Philippe Suter and Olivier Tardieu and Josh Milthorpe},
title = {Distributed Programming in Scala with APGAS},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1317},
doi = {10.1145/2774975.2774977},
year = {2015},
}
Publisher's Version
Article Search


Voirol, Nicolas

SCALA '15: "CounterExample Complete Verification ..."
CounterExample Complete Verification for HigherOrder Functions
Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak
(EPFL, Switzerland)
We present a verification procedure for pure higherorder functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counterexamples. The procedure reduces the analysis of higherorder programs to checking satisfiability of a sequence of quantifierfree formulas over theories such as algebraic data types, integer linear arithmetic, and uninterpreted function symbols, thus enabling the use of efficient satisfiability modulo theory (SMT) solvers. Our solution supports arbitrary function types and arbitrarily nested anonymous functions (which can be stored in data structures, passed as arguments, returned, and applied). Among the contributions of this work is supporting even those cases when anonymous functions cannot be statically traced back to their definition, ensuring completeness of the approach for finding counterexamples. We provide a proof of soundness and counterexample completeness for our system as well as initial evaluation in the Leon verifier.
@InProceedings{SCALA15p18,
author = {Nicolas Voirol and Etienne Kneuss and Viktor Kuncak},
title = {CounterExample Complete Verification for HigherOrder Functions},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1829},
doi = {10.1145/2774975.2774978},
year = {2015},
}
Publisher's Version
Article Search
