Options
Pascal Weisenburger
Last Name
Weisenburger
First name
Pascal
Email
pascal.weisenburger@unisg.ch
ORCID
Phone
+41 71 224 7867
Now showing
1 - 10 of 18
-
PublicationDecentralizing Infrastructure as Code( 2023)Guido SalvaneschiInfrastructure as Code (IaC) automates deployments for single teams, falling short of decentralized deployments across groups. We need mature IaC solutions that embrace and consolidate software engineering principles to enable testing and automation advances for decentralized organizations.Type: journal articleJournal: IEEE SoftwareVolume: 40Issue: 1
-
PublicationTCEP: Transitions in Operator Placement to Adapt to Dynamic Network Environments( 2021)
;Luthra, Manisha ;Koldehofe, Boris ;Danger, NielsStavrakakis, IoannisType: journal articleJournal: Journal of Computer and System SciencesVolume: 122 -
PublicationA Survey of Multitier Programming( 2021)
;Wirth, JohannesType: journal articleJournal: ACM Computing SurveysVolume: 53Issue: 4 -
PublicationRethinking Safe Consistency in Distributed Object-Oriented Programming( 2020)
;Köhler, Mirko ;Eskandani, Nafise ;Margara, AlessandroType: journal articleJournal: Proceedings of the ACM on Programming LanguagesVolume: 4Issue: OOPSLA -
PublicationDistributed System Development with ScalaLoci( 2018)
;Köhler, MirkoType: journal articleJournal: Proceedings of the ACM on Programming LanguagesVolume: 2Issue: OOPSLA -
PublicationType-Checking CRDT Convergence( 2023-06-06)Guido SalvaneschiConflict-Free Replicated Data Types (CRDTs) are a recent approach for keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. For correct operation, CRDTs rely on a merge function that is commutative, associative and idempotent. Ensuring that such algebraic properties are satisfied by implementations, however, is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of a model, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations. In this paper, we present Propel, a programming language with a type system that captures the algebraic properties required by a correct CRDT implementation. The Propel type system deduces such properties by case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction for free. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties. We provide an implementation of Propel as a Scala embedding, we implement several CRDTs, verify them with Propel and compare the verification process with four state-of-the-art verification tools. Our evaluation shows that Propel is able to automatically deduce the properties that are relevant for common CRDT implementations found in open-source libraries even in cases in which competitors timeout.Type: conference paperJournal: Proceedings of the ACM on Programming LanguagesVolume: 7Issue: PLDIDOI: 10.1145/3591276
-
PublicationPrisma: A Tierless Language for Enforcing Contract-client Protocols in Decentralized Apps( 2022-06)
;Richter, David ;Kretzler, David ;Faust, SebastianMezini, MiraType: conference paperVolume: 222 -
PublicationType: conference paper
-
PublicationMultiparty Languages: The Choreographic and Multitier Cases( 2021-07)
;Giallorenzo, Saverio ;Montesi, Fabrizio ;Peressotti, Marco ;Richter, DavidType: conference paperVolume: 194 -
PublicationType: conference paper