Over the past decades, various techniques for the application of formal program analysis of software systems have been proposed. However, the application of formal methods for software verification is still limited in practise. It is acknowledged that the task of formally specifying requirements by creating property specifications and the need of the interaction by the engineer with the prover during the execution of the proof are valid hindrances. The objectives of the presented PhD project are the automated inference of declarative property specifications from example scenarios during the phase of Requirements Engineering and their automated verification on abstract model level and on code level. Applying Inductive Logic Programming, we introduce the necessary modifications and extensions of the methodology in order to enable property specification mining from example data. Example data are to be collected with the guidance by the Scenario Modeling Strategies to ensure the necessary coverage of the scenario that is stated with the application in order to correct use of the provided information in the property specification mining algorithm. However, the specification mining algorithm is expected to produce too many property specifications. To turn the weakness into strength, our approach proposes to use the properties to automate the proof and by this, reduce the necessary interaction with the prover.