| 1. |
- Abolfathi, Bela, et al.
(författare)
-
The Fourteenth Data Release of the Sloan Digital Sky Survey : First Spectroscopic Data from the Extended Baryon Oscillation Spectroscopic Survey and from the Second Phase of the Apache Point Observatory Galactic Evolution Experiment
- 2018
-
Ingår i: Astrophysical Journal Supplement Series. - : IOP Publishing Ltd. - 0067-0049 .- 1538-4365. ; 235:2
-
Tidskriftsartikel (refereegranskat)abstract
- The fourth generation of the Sloan Digital Sky Survey (SDSS-IV) has been in operation since 2014 July. This paper describes the second data release from this phase, and the 14th from SDSS overall (making this Data Release Fourteen or DR14). This release makes the data taken by SDSS-IV in its first two years of operation (2014-2016 July) public. Like all previous SDSS releases, DR14 is cumulative, including the most recent reductions and calibrations of all data taken by SDSS since the first phase began operations in 2000. New in DR14 is the first public release of data from the extended Baryon Oscillation Spectroscopic Survey; the first data from the second phase of the Apache Point Observatory (APO) Galactic Evolution Experiment (APOGEE-2), including stellar parameter estimates from an innovative data-driven machine-learning algorithm known as "The Cannon"; and almost twice as many data cubes from the Mapping Nearby Galaxies at APO (MaNGA) survey as were in the previous release (N = 2812 in total). This paper describes the location and format of the publicly available data from the SDSS-IV surveys. We provide references to the important technical papers describing how these data have been taken (both targeting and observation details) and processed for scientific use. The SDSS web site (www.sdss.org) has been updated for this release and provides links to data downloads, as well as tutorials and examples of data use. SDSS-IV is planning to continue to collect astronomical data until 2020 and will be followed by SDSS-V.
|
|
| 2. |
- Aguado, D. S., et al.
(författare)
-
The Fifteenth Data Release of the Sloan Digital Sky Surveys : First Release of MaNGA-derived Quantities, Data Visualization Tools, and Stellar Library
- 2019
-
Ingår i: Astrophysical Journal Supplement Series. - : Institute of Physics Publishing (IOPP). - 0067-0049 .- 1538-4365. ; 240:2
-
Tidskriftsartikel (refereegranskat)abstract
- Twenty years have passed since first light for the Sloan Digital Sky Survey (SDSS). Here, we release data taken by the fourth phase of SDSS (SDSS-IV) across its first three years of operation (2014 July-2017 July). This is the third data release for SDSS-IV, and the 15th from SDSS (Data Release Fifteen; DR15). New data come from MaNGA-we release 4824 data cubes, as well as the first stellar spectra in the MaNGA Stellar Library (MaStar), the first set of survey-supported analysis products (e.g., stellar and gas kinematics, emission-line and other maps) from the MaNGA Data Analysis Pipeline, and a new data visualization and access tool we call "Marvin." The next data release, DR16, will include new data from both APOGEE-2 and eBOSS; those surveys release no new data here, but we document updates and corrections to their data processing pipelines. The release is cumulative; it also includes the most recent reductions and calibrations of all data taken by SDSS since first light. In this paper, we describe the location and format of the data and tools and cite technical references describing how it was obtained and processed. The SDSS website (www.sdss.org) has also been updated, providing links to data downloads, tutorials, and examples of data use. Although SDSS-IV will continue to collect astronomical data until 2020, and will be followed by SDSS-V (2020-2025), we end this paper by describing plans to ensure the sustainability of the SDSS data archive for many years beyond the collection of data.
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642340253 ; 7609 LNCS:PART 1, s. 312-326
-
Konferensbidrag (refereegranskat)abstract
- Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Selective Presumed Benevolence in Multi-party System Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13701 LNCS, s. 106-123
-
Konferensbidrag (refereegranskat)abstract
- The functional correctness of particular components in a multi-party system may be dependent on the behaviour of other components and parties. Assumptions about how the other parties will act would thus have to be reflected in the specifications. In fact, one can find a substantial body of work on assume-guarantee reasoning with respect to the functional aspects of the component under scrutiny and those of other components. In this paper, we turn to look at non-functional assumptions about the behaviour of other parties. In particular, we look at smart contract verification under assumptions about presumed benevolence of particular parties and focusing on reentrancy issues—a class of bugs which, in the past few years, has led to huge financial losses. We make a case for allowing, in the specification, fine-grained assumptions on benevolence of certain parties, and show how these assumptions can be exploited in the verification process.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Smart Contracts: A Killer Application for Deductive Source Code Verification
- 2018
-
Ingår i: Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday. - Cham : Springer International Publishing. - 9783319980478 ; , s. 1-18
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Smart contracts are agreements between parties which, not only describe the ideal behaviour expected from those parties, but also automates such ideal performance. Blockchain, and similar distributed ledger technologies have enabled the realisation of smart contracts without the need of trusted parties—typically using computer programs which have access to digital assets to describe smart contracts, storing and executing them in a transparent and immutable manner on a blockchain. Many approaches have adopted fully fledged programming languages to describe smart contract, thus inheriting from software the challenge of correctness and verification—just as in software systems, in smart contracts mistakes happen easily, leading to unintended and undesirable behaviour. Such wrong behaviour may show accidentally, but as the contract code is public, malicious users can seek for vulnerabilities to exploit, causing severe damage. This is witnessed by the increasing number of real world incidents, many leading to huge financial losses. As in critical software, the formal verification of smart contracts is thus paramount. In this paper we argue for the use of deductive software verification as a way to increase confidence in the correctness of smart contracts. We describe challenges and opportunities, and a concrete research program, for deductive source code level verification, focussing on the most widely used smart contract platform and language, Ethereum and Solidity.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
StaRVOOrS - Episode II: Strengthen and distribute the force
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319471655 ; 9952, s. 402-415
-
Konferensbidrag (refereegranskat)abstract
- Static and runtime techniques for the verification of programs are complementary. They both have their advantages and disadvantages, and a natural question is whether they may be combined in such a way as to get the advantages of both without inheriting too much from their disadvantages. In a previous contribution to ISoLA’12, we have proposed StaRVOOrS (‘Static and Runtime Verification of Object- Oriented Software’), a unified framework for combining static and runtime verification in order to check data- and control-oriented properties. Returning to ISoLA here, we briefly report on advances since then: a unified specification language for data- and control-oriented properties, a tool for combined static and runtime verification, and experiments. On that basis, we discuss two future research directions to strengthen the power, and broaden the scope, of combined static and runtime verification: (i) to use static analysis techniques to further optimise the runtime monitor, and (ii) to extend the framework to the distributed case.
|
|
| 7. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11761 LNCS, s. 228-243
-
Konferensbidrag (refereegranskat)abstract
- Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY’s native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity.
|
|
| 8. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS, volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
-
Konferensbidrag (refereegranskat)abstract
- Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
|
|
| 9. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
On the Specification and Monitoring of Timed Normative Systems
- 2021
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.
|
|
| 10. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Runtime Monitoring Processes Across Blockchains
- 2021
-
Ingår i: 9th IPM International Conference on Fundamentals of Software Engineering 2021 (FSEN 2021). - Cham : Springer International Publishing.
-
Konferensbidrag (refereegranskat)abstract
- Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a setup is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated. As blockchain platforms mature and their applications increase, one can observe that instead of having one blockchain as a ‘one world computer’ multiple blockchains will co-exist while possibly interacting. Existing work for business processes within the blockchain domain have focused on single isolated blockchain implementations. In this paper, we do away with this severely limiting assumption and propose a method to monitor business processes spanning different blockchains and other off-chain servers. We apply this work to business processes expressed in BPMN along with annotations proposed for a blockchain context. We further describe how we handle blockchain interoperability by synthesizing automatically off-chain monitors, acting as notaries, that handle message passing between blockchain systems, and how we employ hash-locking for cryptographically secure token swapping.
|
|
